let L be AD_Lattice; :: thesis: for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x )
let x, y be Element of L; :: thesis: ( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x )
hereby :: thesis: ( x "/\" (y "\/" x) = x implies (x "/\" y) "\/" x = x )
assume A1: (x "/\" y) "\/" x = x ; :: thesis: x "/\" (y "\/" x) = x
x "/\" (y "\/" x) = (x "/\" y) "\/" (x "/\" x) by LATTICES:def 11
.= x by A1, IMeet ;
hence x "/\" (y "\/" x) = x ; :: thesis: verum
end;
assume A1: x "/\" (y "\/" x) = x ; :: thesis: (x "/\" y) "\/" x = x
(x "/\" y) "\/" x = (x "/\" y) "\/" (x "/\" x) by IMeet
.= x "/\" (y "\/" x) by LATTICES:def 11 ;
hence (x "/\" y) "\/" x = x by A1; :: thesis: verum