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 meet-commutative implies L is meet-commutative )
assume that
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 #) and
A2: K is meet-commutative ; :: thesis: L is meet-commutative
L is meet-commutative
proof
let x, y be Element of L; :: according to LATTICES:def 6 :: thesis: x |^| y = y |^| x
reconsider x9 = x, y9 = y as Element of K by A1;
x9 "/\" y9 = y9 "/\" x9 by A2;
hence x |^| y = y |^| x by A1; :: thesis: verum
end;
hence L is meet-commutative ; :: thesis: verum