proposition: Lemma class_of_sub : forall (a : E) (r : E2P) (y z : E), inc y z -> is_part a r z -> sub (class_of a r y) z.
proof: Proof. ir. unfold class_of in |- *. ap intersection_sub. ap inc_parts_containing; au. Qed.
imports: set_theory