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:26;
H1(L1) absorbs H2(L1)
by LATTICE2:26;
then A2:
H1(LL) absorbs H2(LL)
by A1, Th30;
A3:
H1(LL) is associative
by Th23;
A4:
H2(L2) absorbs H1(L2)
by LATTICE2:27;
H2(L1) absorbs H1(L1)
by LATTICE2:27;
then A5:
H2(LL) absorbs H1(LL)
by A4, Th30;
A6:
H2(LL) is commutative
by Th22;
A7:
H2(LL) is associative
by Th23;
H1(LL) is commutative
by Th22;
hence
[:L1,L2:] is Lattice-like
by A3, A6, A7, A2, A5, LATTICE2:11; verum