reconsider LL = LattStr(# [:the carrier of L1,the carrier of L2:],|:the L_join of L1,the L_join of L2:|,|:the L_meet of L1,the L_meet of L2:| #) as non empty LattStr ;
A1:
H1(L2) absorbs H2(L2)
by LATTICE2:40;
H1(L1) absorbs H2(L1)
by LATTICE2:40;
then A2:
H1(LL) absorbs H2(LL)
by A1, Th31;
A3:
H1(LL) is associative
by Th24;
A4:
H2(L2) absorbs H1(L2)
by LATTICE2:41;
H2(L1) absorbs H1(L1)
by LATTICE2:41;
then A5:
H2(LL) absorbs H1(LL)
by A4, Th31;
A6:
H2(LL) is commutative
by Th23;
A7:
H2(LL) is associative
by Th24;
H1(LL) is commutative
by Th23;
hence
[:L1,L2:] is Lattice-like
by A3, A6, A7, A2, A5, LATTICE2:17; :: thesis: verum