Thm* f:(AB), R:(BBProp). Bij(A; B; f) (EquivRel x,y:B. x R y) (F:((x,y:A//(x R_f y))(x,y:B//(x R y))). Bij(x,y:A//(x R_f y); x,y:B//(x R y); F)) quotient_1_1_corr

Thm* f:(AB), R:(BBProp). (EquivRel x,y:B. x R y) (EquivRel x,y:A. x R_f y) preima_of_equiv_rel