let L be GAD_Lattice; :: thesis: ( L is join-commutative iff L is meet-commutative )

hereby :: thesis: ( L is meet-commutative implies L is join-commutative )

assume A1: L is join-commutative ; :: thesis: L is meet-commutative
thus L is meet-commutative :: thesis: verum

proof

let a, b be Element of L; :: according to LATTICES:def 6 :: thesis: a "/\" b = b "/\" a
a "\/" b = b "\/" a by A1;
then (a "/\" b) "\/" a = a by Th3716;
hence a "/\" b = b "/\" a by Th3715; :: thesis: verum

end;

end;

assume B1: L is meet-commutative ; :: thesis: L is join-commutative
let a, b be Element of L; :: according to LATTICES:def 4 :: thesis: a "\/" b = b "\/" a
a "/\" b = b "/\" a by B1;
then (a "/\" b) "\/" a = a by LATTICES:def 8;
hence a "\/" b = b "\/" a by Th3716; :: thesis: verum