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