let L be AD_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 "/\" (y "\/" x)) "\/" (y "/\" (y "\/" x)) by Ze, A0
.= (x "\/" y) "/\" (y "\/" x) by DefD
.= ((x "\/" y) "/\" y) "\/" ((x "\/" y) "/\" x) by LATTICES:def 11
.= y "\/" ((x "\/" y) "/\" x) by DefA1
.= y "\/" x by DefA2 ;
hence x "\/" y = y "\/" x ; :: thesis: verum