let L be with_zero GAD_Lattice; :: thesis: for x, y being Element of L st x "/\" y = bottom L holds
x "\/" y = y "\/" x
let x, y be Element of L; :: thesis: ( x "/\" y = bottom L implies x "\/" y = y "\/" x )
assume x "/\" y = bottom L ; :: thesis: x "\/" y = y "\/" x
then (y "/\" x) "\/" y = y by Th3751, Lem316;
hence x "\/" y = y "\/" x by Th3716; :: thesis: verum