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