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 )

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

thus
( U1 is SubAlgebra of U2 implies l1 [= l2 )
:: thesis: verum
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;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

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;then the carrier of U1 is Subset of U2 by UNIALG_2:def 7;

hence l1 [= l2 by A1, Th15; :: thesis: verum