let L be GAD_Lattice; :: thesis: for x, y being Element of L holds
( x "\/" y = y "\/" x iff ( ex_lub_of x,y & x "\/" y = lub (x,y) ) )
let x, y be Element of L; :: thesis: ( x "\/" y = y "\/" x iff ( ex_lub_of x,y & x "\/" y = lub (x,y) ) )

hereby :: thesis: ( ex_lub_of x,y & x "\/" y = lub (x,y) implies x "\/" y = y "\/" x )

assume x "\/" y = y "\/" x ; :: thesis: ( ex_lub_of x,y & x "\/" y = lub (x,y) )
then ex c being Element of L st
( x [= c & y [= c ) by Th3823, LemX3;
hence ( ex_lub_of x,y & x "\/" y = lub (x,y) ) by Th3834; :: thesis: verum

end;

assume ( ex_lub_of x,y & x "\/" y = lub (x,y) ) ; :: thesis: x "\/" y = y "\/" x
hence x "\/" y = y "\/" x by Th3841; :: thesis: verum