let L be GAD_Lattice; :: thesis: for x, y being Element of L holds
( x "\/" y = y "\/" x iff y [= x "\/" y )
let x, y be Element of L; :: thesis: ( x "\/" y = y "\/" x iff y [= x "\/" y )
thus ( x "\/" y = y "\/" x implies y [= x "\/" y ) by LemX3; :: thesis: ( y [= x "\/" y implies x "\/" y = y "\/" x )
assume y [= x "\/" y ; :: thesis: x "\/" y = y "\/" x
then ex z being Element of L st
( x [= z & y [= z ) by Th3823;
hence x "\/" y = y "\/" x by DefB2; :: thesis: verum