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 (x "/\" y) "\/" x = x ; :: thesis: x "/\" y = y "/\" x
then y "/\" x = (y "/\" (x "/\" y)) "\/" (y "/\" x) by LATTICES:def 11
.= (x "/\" y) "\/" (y "/\" x) by Lem36c
.= (x "/\" y) "\/" (x "/\" (y "/\" x)) by Lem36c
.= x "/\" (y "\/" (y "/\" x)) by LATTICES:def 11
.= x "/\" y by ThA4 ;
hence x "/\" y = y "/\" x ; :: thesis: verum