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 )

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

( the carrier of U1 c= the carrier of U2 implies l1 [= l2 )
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;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

proof

hence
( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff the carrier of U1 c= the carrier of U2 ) )
by A1; :: thesis: verum
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;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