theorem Th11: :: LATTICE2:11

for L being non empty LattStr st the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L holds
L is Lattice-like