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 )
reconsider LL = LattStr(# [:the carrier of L1,the carrier of L2:],|:H1(L1),H1(L2):|,|:H2(L1),H2(L2):| #) as non empty LattStr ;
( H1(LL) is commutative & H1(LL) is associative & H2(LL) is commutative & H2(LL) is associative & H1(LL) absorbs H2(LL) & H2(LL) absorbs H1(LL) )
by A1, LATTICE2:40, LATTICE2:41;
then
( H1(L1) is commutative & H1(L1) is associative & H2(L1) is commutative & H2(L1) is associative & H1(L1) absorbs H2(L1) & H2(L1) absorbs H1(L1) & H1(L2) is commutative & H1(L2) is associative & H2(L2) is commutative & H2(L2) is associative & H1(L2) absorbs H2(L2) & H2(L2) absorbs H1(L2) )
by Th23, Th24, Th31;
hence
( L1 is Lattice & L2 is Lattice )
by LATTICE2:17; :: thesis: verum