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: H1(L1) is associative by A1, Th23;
A3: H2(L2) is associative by A1, Th23;
A4: H2(L2) is commutative by A1, Th22;
reconsider LL = LattStr(# [: the carrier of L1, the carrier of L2:],|:H1(L1),H1(L2):|,|:H2(L1),H2(L2):| #) as non empty LattStr ;
A5: H1(LL) absorbs H2(LL) by A1, LATTICE2:26;
then A6: H1(L1) absorbs H2(L1) by Th30;
A7: H1(L2) is associative by A1, Th23;
A8: H1(L2) is commutative by A1, Th22;
A9: H2(L1) is associative by A1, Th23;
A10: H2(L1) is commutative by A1, Th22;
A11: H2(LL) absorbs H1(LL) by A1, LATTICE2:27;
then A12: H2(L1) absorbs H1(L1) by Th30;
A13: H2(L2) absorbs H1(L2) by A11, Th30;
A14: H1(L2) absorbs H2(L2) by A5, Th30;
H1(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