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

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

assume x "\/" y = y "\/" x ; :: thesis: ( ex_lub_of x,y & y "\/" x = lub (x,y) )
then x [= y "\/" x by LemX3;
hence ( ex_lub_of x,y & y "\/" x = lub (x,y) ) by Th3856; :: thesis: verum

end;

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