let U0 be with_const_op Universal_Algebra; :: thesis: for l1, l2 being Element of (UnSubAlLattice U0)
for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff the carrier of U1 c= the carrier of U2 )
let l1, l2 be Element of (UnSubAlLattice U0); :: thesis: for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds
( l1 [= l2 iff the carrier of U1 c= the carrier of U2 )
let U1, U2 be strict SubAlgebra of U0; :: thesis: ( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff the carrier of U1 c= the carrier of U2 ) )
reconsider l1 = U1 as Element of (UnSubAlLattice U0) by UNIALG_2:def 14;
reconsider l2 = U2 as Element of (UnSubAlLattice U0) by UNIALG_2:def 14;
A1: ( l1 [= l2 implies the carrier of U1 c= the carrier of U2 )

proof

reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 7;
reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;
reconsider U3 = U11 \/ U21 as non empty Subset of U0 ;
assume l1 [= l2 ; :: thesis: the carrier of U1 c= the carrier of U2
then l1 "\/" l2 = l2 ;
then U1 "\/" U2 = U2 by UNIALG_2:def 15;
then GenUnivAlg U3 = U2 by UNIALG_2:def 13;
then A2: the carrier of U1 \/ the carrier of U2 c= the carrier of U2 by UNIALG_2:def 12;
the carrier of U2 c= the carrier of U1 \/ the carrier of U2 by XBOOLE_1:7;
then the carrier of U1 \/ the carrier of U2 = the carrier of U2 by A2;
hence the carrier of U1 c= the carrier of U2 by XBOOLE_1:7; :: thesis: verum

end;

( the carrier of U1 c= the carrier of U2 implies l1 [= l2 )

proof

reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 7;
reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;
reconsider U3 = U11 \/ U21 as non empty Subset of U0 ;
assume the carrier of U1 c= the carrier of U2 ; :: thesis: l1 [= l2
then GenUnivAlg U3 = U2 by UNIALG_2:19, XBOOLE_1:12;
then U1 "\/" U2 = U2 by UNIALG_2:def 13;
then l1 "\/" l2 = l2 by UNIALG_2:def 15;
hence l1 [= l2 ; :: thesis: verum

end;

hence ( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff the carrier of U1 c= the carrier of U2 ) ) by A1; :: thesis: verum