let L be GAD_Lattice; :: thesis: for x, y being Element of L st x "/\" (y "\/" x) = x holds
x "\/" y = y "\/" x
let x, y be Element of L; :: thesis: ( x "/\" (y "\/" x) = x implies x "\/" y = y "\/" x )
assume A0: x "/\" (y "\/" x) = x ; :: thesis: x "\/" y = y "\/" x
(x "/\" y) "\/" x = x by Th3712, A0;
then (y "/\" x) "\/" y = y by Th3713;
then a3: y "/\" (x "\/" y) = y by Th3712;
y "\/" x = y "\/" ((x "\/" y) "/\" x) by DefA2
.= (y "\/" (x "\/" y)) "/\" (y "\/" x) by DefLDS
.= (x "\/" y) "/\" (y "\/" x) by a3, LATTICES:def 8
.= (x "\/" y) "/\" (x "\/" (y "\/" x)) by A0, LATTICES:def 8
.= x "\/" (y "/\" (y "\/" x)) by DefLDS
.= x "\/" y by LATTICES:def 9 ;
hence x "\/" y = y "\/" x ; :: thesis: verum