let L be AD_Lattice; :: thesis: for x, y being Element of L st x [= y holds
x "\/" y = y "\/" x
let x, y be Element of L; :: thesis: ( x [= y implies x "\/" y = y "\/" x )
assume A1: x [= y ; :: thesis: x "\/" y = y "\/" x
ex c being Element of L st
( x [= c & y [= c )

proof

take y ; :: thesis: ( x [= y & y [= y )
thus ( x [= y & y [= y ) by A1, ISum; :: thesis: verum

end;

hence x "\/" y = y "\/" x by Hehe1; :: thesis: verum