THM	incl_aux1_quo	T:. E:T T . x:T. EquivRel(T;x,y.x E y) x x,y:T//(x E y)
THM	incl_aux2_quo	n:{1...}. m:n. E:n n . EquivRel(n;x,y.x E y) (z:x,y:m//(x E y). z x,y:n//(x E y))
THM	incl_aux3_quo	n:{1...}. m:n. E:n n . EquivRel(n;i,j.i E j) (x,y:i,j:m//(i E j). x = y x = y)
THM	incl_aux4_quo	n:{1...}. E:n n . EquivRel(n;i,j.i E j) (x:i,j:n//(i E j). (x = n - 1) x i,j:(n - 1)//(i E j))
THM	incl_aux5_quo	T:. E:T T . EquivRel(T;x,y.x E y) (x,y:T. x = y x = y)
THM	incl_aux6_quo	T:. R:T T . EquivRel(T;x,y.x R y) (Q:x,y:T//(x R y) x,y:T//(x R y) EquivRel(x,y:T//(x R y);u,v.u Q v) EquivRel(T;x,y.x Q y))
THM	rest_refl_rel	n:{1...}. m:n. E:n n . Refl(n;x,y.x E y) Refl(m;x,y.x E y)
THM	rest_symm_rel	n:{1...}. m:n. E:n n . Sym(n;x,y.x E y) Sym(m;x,y.x E y)
THM	rest_tran_rel	n:{1...}. m:n. E:n n . Trans(n;x,y.x E y) Trans(m;x,y.x E y)
THM	rest_equi_rel	n:{1...}. m:n. E:n n . EquivRel(n;x,y.x E y) EquivRel(m;x,y.x E y)
THM	quotient_of_nsubn	n:{1...}. E:n n . EquivRel(n;x,y.x E y) (x,y:n. Dec(x E y)) (m:(n + 1). 1-1-Corresp(m;i,j:n//(i E j)))
THM	quo_of_quo	T:. R:T T . EquivRel(T;x,y.x R y) (Q:x,y:T//(x R y) x,y:T//(x R y) EquivRel(x,y:T//(x R y);u,v.u Q v) 1-1-Corresp(x,y:T//(x Q y);u,v:x,y:T//(x R y)//(u Q v)))
DISP	preima_of_rel_df	<R:R:*>_<f:f:*>== <R>_<f>
ABS	preima_of_rel	R_f == x,y.(f x) R (f y)
THM	preima_of_rel_wf	A,B:. f:A B. R:B B . R_f A A
THM	preima_of_equiv_rel	A,B:. f:A B. R:B B . EquivRel(B;x,y.x R y) EquivRel(A;x,y.x R_f y)
THM	one_one_corr_refl	A:. 1-1-Corresp(A;A)
THM	one_one_corr_symm	A,B:. 1-1-Corresp(A;B) 1-1-Corresp(B;A)
THM	one_one_corr_tran	A,B,C:. 1-1-Corresp(A;B) 1-1-Corresp(B;C) 1-1-Corresp(A;C)
THM	quotient_1_1_corr	A,B:. f:A B. R:B B . Bij(A;B;f) EquivRel(B;x,y.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))
THM	quotient_of_finite	n:{1...}. A:. R:A A . 1-1-Corresp(n;A) EquivRel(A;x,y.x R y) (x,y:A. Dec(x R y)) (m:(n + 1). 1-1-Corresp(m;x,y:A//(x R y)))
COM	hr	Solo para insertar los objetos
THM	fun_aux_1	T,S,T1:. f,g:T S. T1 T f = g f = g

the other theories