let L be GAD_Lattice; :: thesis: ( L is join-commutative iff L is ADL-absorbing )
thus ( L is join-commutative implies L is ADL-absorbing ) :: thesis: ( L is ADL-absorbing implies L is join-commutative )
proof
assume A1: L is join-commutative ; :: thesis: L is ADL-absorbing
let a, b be Element of L; :: according to LATTAD_1:def 5 :: thesis: a "/\" (b "\/" a) = a
a "\/" b = b "\/" a by A1;
hence a "/\" (b "\/" a) = a by LATTICES:def 9; :: thesis: verum
end;
assume B1: L is ADL-absorbing ; :: thesis: L is join-commutative
let a, b be Element of L; :: according to LATTICES:def 4 :: thesis: a "\/" b = b "\/" a
a "/\" (b "\/" a) = a by B1;
hence a "\/" b = b "\/" a by Th3726; :: thesis: verum