let L be GAD_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 )
thus ( (x "/\" y) "\/" x = x implies x "/\" (y "\/" x) = x ) :: thesis: ( x "/\" (y "\/" x) = x implies (x "/\" y) "\/" x = x )

proof

assume A1: (x "/\" y) "\/" x = x ; :: thesis: x "/\" (y "\/" x) = x
x "/\" (y "\/" x) = (x "/\" y) "\/" (x "/\" x) by LATTICES:def 11
.= (x "/\" y) "\/" x by IMeet ;
hence x "/\" (y "\/" x) = x by A1; :: 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