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 A1: ( 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
( 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 A1, Th9, Th10, Th11, Th12, Th13, Th14;
hence L is Lattice-like ; :: thesis: verum