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