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