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 U1 is SubAlgebra 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 U1 is SubAlgebra of U2 )
let U1, U2 be strict SubAlgebra of U0; :: thesis: ( l1 = U1 & l2 = U2 implies ( l1 [= l2 iff U1 is SubAlgebra of U2 ) )
assume A1: ( l1 = U1 & l2 = U2 ) ; :: thesis: ( l1 [= l2 iff U1 is SubAlgebra of U2 )
thus ( l1 [= l2 implies U1 is SubAlgebra of U2 ) :: thesis: ( U1 is SubAlgebra of U2 implies l1 [= l2 )
proof
assume l1 [= l2 ; :: thesis: U1 is SubAlgebra of U2
then the carrier of U1 c= the carrier of U2 by A1, Th15;
hence U1 is SubAlgebra of U2 by UNIALG_2:11; :: thesis: verum
end;
thus ( U1 is SubAlgebra of U2 implies l1 [= l2 ) :: thesis: verum
proof
assume U1 is SubAlgebra of U2 ; :: thesis: l1 [= l2
then the carrier of U1 is Subset of U2 by UNIALG_2:def 7;
hence l1 [= l2 by A1, Th15; :: thesis: verum
end;