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-commutative implies L is join-commutative )
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-commutative ) ; :: thesis: L is join-commutative
L is join-commutative

proof

let x, y be Element of L; :: according to LATTICES:def 4 :: thesis: x |_| y = y |_| x
reconsider x' = x, y' = y as Element of K by A1;
x' |_| y' = y' |_| x' by A1, LATTICES:def 4;
hence x |_| y = y |_| x by A1; :: thesis: verum

end;

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