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

proof

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

end;

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