let L be GAD_Lattice; :: thesis: for x, y being Element of L st x [= y "\/" x holds
( ex_lub_of x,y & y "\/" x = lub (x,y) )
let x, y be Element of L; :: thesis: ( x [= y "\/" x implies ( ex_lub_of x,y & y "\/" x = lub (x,y) ) )
assume A1: x [= y "\/" x ; :: thesis: ( ex_lub_of x,y & y "\/" x = lub (x,y) )
A2: y [= y "\/" x by LemX3;
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 = y "\/" x; :: thesis: ( x [= c & y [= c & ( for d being Element of L st x [= d & y [= d holds
c [= d ) )
thus ( x [= c & y [= c ) by A1, 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 LATTICES:def 8; :: thesis: verum
end;
hence A3: ex_lub_of x,y ; :: thesis: y "\/" x = lub (x,y)
for c being Element of L st x [= c & y [= c holds
y "\/" x [= c
proof
let c be Element of L; :: thesis: ( x [= c & y [= c implies y "\/" x [= c )
assume B1: ( x [= c & y [= c ) ; :: thesis: y "\/" x [= c
then (y "\/" x) "/\" c = y "\/" (x "/\" c) by DefLDS
.= y "\/" x by B1, LATTICES:def 9 ;
hence y "\/" x [= c by LATTICES:def 8; :: thesis: verum
end;
hence y "\/" x = lub (x,y) by DefLUB, A1, A2, A3; :: thesis: verum