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: H_{1}(L2) absorbs H_{2}(L2)
by LATTICE2:26;

H_{1}(L1) absorbs H_{2}(L1)
by LATTICE2:26;

then A2: H_{1}(LL) absorbs H_{2}(LL)
by A1, Th30;

A3: H_{1}(LL) is associative
by Th23;

A4: H_{2}(L2) absorbs H_{1}(L2)
by LATTICE2:27;

H_{2}(L1) absorbs H_{1}(L1)
by LATTICE2:27;

then A5: H_{2}(LL) absorbs H_{1}(LL)
by A4, Th30;

A6: H_{2}(LL) is commutative
by Th22;

A7: H_{2}(LL) is associative
by Th23;

H_{1}(LL) is commutative
by Th22;

hence [:L1,L2:] is Lattice-like by A3, A6, A7, A2, A5, LATTICE2:11; :: thesis: verum

A1: H

H

then A2: H

A3: H

A4: H

H

then A5: H

A6: H

A7: H

H

hence [:L1,L2:] is Lattice-like by A3, A6, A7, A2, A5, LATTICE2:11; :: thesis: verum