let L1, L2 be non empty LattStr ; :: thesis: ( [:L1,L2:] is Lattice implies ( L1 is Lattice & L2 is Lattice ) )

assume A1: [:L1,L2:] is Lattice ; :: thesis: ( L1 is Lattice & L2 is Lattice )

A2: H_{1}(L1) is associative
by A1, Th23;

A3: H_{2}(L2) is associative
by A1, Th23;

A4: H_{2}(L2) is commutative
by A1, Th22;

reconsider LL = LattStr(# [: the carrier of L1, the carrier of L2:],|:H_{1}(L1),H_{1}(L2):|,|:H_{2}(L1),H_{2}(L2):| #) as non empty LattStr ;

A5: H_{1}(LL) absorbs H_{2}(LL)
by A1, LATTICE2:26;

then A6: H_{1}(L1) absorbs H_{2}(L1)
by Th30;

A7: H_{1}(L2) is associative
by A1, Th23;

A8: H_{1}(L2) is commutative
by A1, Th22;

A9: H_{2}(L1) is associative
by A1, Th23;

A10: H_{2}(L1) is commutative
by A1, Th22;

A11: H_{2}(LL) absorbs H_{1}(LL)
by A1, LATTICE2:27;

then A12: H_{2}(L1) absorbs H_{1}(L1)
by Th30;

A13: H_{2}(L2) absorbs H_{1}(L2)
by A11, Th30;

A14: H_{1}(L2) absorbs H_{2}(L2)
by A5, Th30;

H_{1}(L1) is commutative
by A1, Th22;

hence ( L1 is Lattice & L2 is Lattice ) by A2, A10, A9, A6, A12, A8, A7, A4, A3, A14, A13, LATTICE2:11; :: thesis: verum

assume A1: [:L1,L2:] is Lattice ; :: thesis: ( L1 is Lattice & L2 is Lattice )

A2: H

A3: H

A4: H

reconsider LL = LattStr(# [: the carrier of L1, the carrier of L2:],|:H

A5: H

then A6: H

A7: H

A8: H

A9: H

A10: H

A11: H

then A12: H

A13: H

A14: H

H

hence ( L1 is Lattice & L2 is Lattice ) by A2, A10, A9, A6, A12, A8, A7, A4, A3, A14, A13, LATTICE2:11; :: thesis: verum