let L be AD_Lattice; :: thesis: for x, y being Element of L st ex z being Element of L st
( x [= z & y [= z ) holds
x "\/" y = y "\/" x
let x, y be Element of L; :: thesis: ( ex z being Element of L st
( x [= z & y [= z ) implies x "\/" y = y "\/" x )
assume A0: ex z being Element of L st
( x [= z & y [= z ) ; :: thesis: x "\/" y = y "\/" x
y "/\" (x "\/" y) = y
proof
consider z being Element of L such that
A1: ( x [= z & y [= z ) by A0;
thus y "/\" (x "\/" y) = (y "/\" x) "\/" (y "/\" y) by LATTICES:def 11
.= (y "/\" x) "\/" y by IMeet
.= (y "/\" x) "\/" (y "/\" z) by A1, Lem232
.= y "/\" (x "\/" z) by LATTICES:def 11
.= y by A1, Lem232 ; :: thesis: verum
end;
hence x "\/" y = y "\/" x by Th1726; :: thesis: verum