proposition: Lemma inc_morphism_set1 : forall r, inc r morphism_set = exists a, exists b, (inc a obs & inc b obs & inc r (homs a b)).
proof: Proof. ir. ap iff_eq; ir. ufi morphism_set H. nin (union_exists H). ee. rwi inc_morphism_set_pool H1. nin H1. nin H1. ee. sh x0. sh x1. ee; try am. wrr H3. nin H. nin H. ee. uf morphism_set. apply union_inc with (homs x x0). am. rw inc_morphism_set_pool. sh x. sh x0. ee; try am; try tv. Qed.
imports: Arith ordinal nat_trans