let L be GAD_Lattice; :: thesis: for x, y being Element of L st ex c being Element of L st
( x [= c & y [= c ) holds
( ex_lub_of x,y & x "\/" y = lub (x,y) )
let x, y be Element of L; :: thesis: ( ex c being Element of L st
( x [= c & y [= c ) implies ( ex_lub_of x,y & x "\/" y = lub (x,y) ) )
given c being Element of L such that A0: ( x [= c & y [= c ) ; :: thesis: ( ex_lub_of x,y & x "\/" y = lub (x,y) )
ex c being Element of L st
( x [= c & y [= c & ( for d being Element of L st x [= d & y [= d holds
c [= d ) )

proof

take c = x "\/" y; :: thesis: ( x [= c & y [= c & ( for d being Element of L st x [= d & y [= d holds
c [= d ) )
S1: x "\/" y = y "\/" x by A0, DefB2;
hence ( x [= c & y [= c ) by LemX3; :: thesis: for d being Element of L st x [= d & y [= d holds
c [= d
let d be Element of L; :: thesis: ( x [= d & y [= d implies c [= d )
assume B1: ( x [= d & y [= d ) ; :: thesis: c [= d
then (y "\/" x) "/\" d = y "\/" (x "/\" d) by DefLDS
.= y "\/" x by B1, LATTICES:def 9 ;
hence c [= d by S1, LATTICES:def 8; :: thesis: verum

end;

hence A3: ex_lub_of x,y ; :: thesis: x "\/" y = lub (x,y)
x "\/" y = y "\/" x by A0, DefB2;
then B2: ( x [= x "\/" y & y [= x "\/" y ) by LemX3;
for c being Element of L st x [= c & y [= c holds
x "\/" y [= c

proof

let c be Element of L; :: thesis: ( x [= c & y [= c implies x "\/" y [= c )
assume B1: ( x [= c & y [= c ) ; :: thesis: x "\/" y [= c
then (x "\/" y) "/\" c = x "\/" (y "/\" c) by DefLDS
.= x "\/" y by B1, LATTICES:def 9 ;
hence x "\/" y [= c by LATTICES:def 8; :: thesis: verum

end;

hence x "\/" y = lub (x,y) by DefLUB, A3, B2; :: thesis: verum