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 join-associative implies L is join-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 join-associative ; :: thesis: L is join-associative
L is join-associative
proof
let x, y, z be Element of L; :: according to LATTICES:def 5 :: 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 join-associative ; :: thesis: verum