let L be GAD_Lattice; :: thesis:
let x, y be Element of L; :: thesis:
given c being Element of L such that A0: ( x [= c & y [= c ) ; :: thesis:
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 ) )

take c = x "\/" y; :: thesis:
S1: x "\/" y = y "\/" x by A0, DefB2;
hence ( x [= c & y [= c ) by LemX3; :: thesis:
let d be Element of L; :: thesis:
assume B1: ( x [= d & y [= d ) ; :: thesis:
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:

end;

hence A3: ex_lub_of x,y ; :: thesis:
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

let c be Element of L; :: thesis:
assume B1: ( x [= c & y [= c ) ; :: thesis:
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:

end;

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