let K, L be non empty LattStr ; :: thesis: ( 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 implies L is Lattice-like )
assume ( 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 ) ; :: thesis: L is Lattice-like
then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by Th9, Th10, Th11, Th12, Th13, Th14;
hence L is Lattice-like ; :: thesis: verum