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-associative implies L is meet-associative )
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-associative ; :: thesis: L is meet-associative
L is meet-associative

proof

let x, y, z be Element of L; :: according to LATTICES:def 7 :: thesis: x |^| (y |^| z) = (x |^| y) |^| z
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
(x9 "/\" y9) "/\" z9 = x9 "/\" (y9 "/\" z9) by A2;
hence x |^| (y |^| z) = (x |^| y) |^| z by A1; :: thesis: verum

end;

hence L is meet-associative ; :: thesis: verum