let L be GAD_Lattice; :: thesis: for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "\/" y = y "\/" x )
let x, y be Element of L; :: thesis: ( (x "/\" y) "\/" x = x iff x "\/" y = y "\/" x )

hereby :: thesis: ( x "\/" y = y "\/" x implies (x "/\" y) "\/" x = x )

assume A1: (x "/\" y) "\/" x = x ; :: thesis: x "\/" y = y "\/" x
x "/\" (y "\/" x) = x by A1, Th3712;
hence x "\/" y = y "\/" x by Th3726; :: thesis: verum

end;

assume x "\/" y = y "\/" x ; :: thesis: (x "/\" y) "\/" x = x
then x "/\" (y "\/" x) = x by LATTICES:def 9;
hence (x "/\" y) "\/" x = x by Th3712; :: thesis: verum