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 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 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 x' = x, y' = y, z' = z as Element of K by A1;
(x' |_| y') |_| z' = x' |_| (y' |_| z') by A1, LATTICES:def 5;
hence x |_| (y |_| z) = (x |_| y) |_| z by A1; :: thesis: verum

end;

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