theorem
for
K,
L being non
empty LattStr st
LattStr(# the
carrier of
K, the
L_join of
K, the
L_meet of
K #)
= LattStr(# the
carrier of
L, the
L_join of
L, the
L_meet of
L #) &
K is
Lattice-like holds
L is
Lattice-like by Th9, Th10, Th11, Th12, Th13, Th14;