proposition: Lemma Surj_epic : forall h : B -> A, Surj_law f h -> SET_Epic_law f.
proof: Proof. intros h H; unfold Surj_law, SET_Epic_law, Epic_law in |- *; intros a f' f'' H1. simpl in |- *; unfold Ext in |- *; intro x. apply Trans with (f' (f (h x))). apply Pres1; apply H. apply Trans with (f'' (f (h x))). exact (H1 (h x)). apply Pres1; apply Sym; apply H. Qed.
imports: SET CatProperty MapProperty