let L be non empty Poset; :: thesis: ( ( L is with_suprema or L is /\-complete ) implies for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z ) )
assume A1: ( L is with_suprema or L is /\-complete ) ; :: thesis: for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z )
let x, y, z be Element of L; :: thesis: ( x << z & y << z implies ( ex_sup_of {x,y},L & x "\/" y << z ) )
assume A2: z >> x ; :: thesis: ( not y << z or ( ex_sup_of {x,y},L & x "\/" y << z ) )
then A3: ( z >= x & ( for D being non empty directed Subset of L st z <= sup D holds
ex d being Element of L st
( d in D & x <= d ) ) ) by Def1, Th1;
assume A4: z >> y ; :: thesis: ( ex_sup_of {x,y},L & x "\/" y << z )
then A5: ( z >= y & ( for D being non empty directed Subset of L st z <= sup D holds
ex d being Element of L st
( d in D & y <= d ) ) ) by Def1, Th1;

hereby :: thesis: x "\/" y << z

per cases ( L is with_suprema or L is /\-complete ) by A1;

suppose L is with_suprema ; :: thesis: ex_sup_of {x,y},L

hence ex_sup_of {x,y},L by YELLOW_0:20; :: thesis: verum

end;

suppose A7: L is /\-complete ; :: thesis: ex_sup_of {x,y},L

set X = { a where a is Element of L : ( a >= x & a >= y ) } ;
{ a where a is Element of L : ( a >= x & a >= y ) } c= the carrier of L

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { a where a is Element of L : ( a >= x & a >= y ) } or a in the carrier of L )
assume a in { a where a is Element of L : ( a >= x & a >= y ) } ; :: thesis: a in the carrier of L
then ex z being Element of L st
( a = z & z >= x & z >= y ) ;
hence a in the carrier of L ; :: thesis: verum

end;

then reconsider X = { a where a is Element of L : ( a >= x & a >= y ) } as Subset of L ;
z in X by A3, A5;
then ex_inf_of X,L by A7, WAYBEL_0:76;
then consider c being Element of L such that
A8: c is_<=_than X and
A9: for d being Element of L st d is_<=_than X holds
d <= c by YELLOW_0:16;
A10: c is_>=_than {x,y}

proof

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in {x,y} or a <= c )
assume A11: a in {x,y} ; :: thesis: a <= c
a is_<=_than X

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in X or a <= b )
assume b in X ; :: thesis: a <= b
then ex z being Element of L st
( b = z & z >= x & z >= y ) ;
hence a <= b by A11, TARSKI:def 2; :: thesis: verum

end;

hence a <= c by A9; :: thesis: verum

end;

now

let a be Element of L; :: thesis: ( a is_>=_than {x,y} implies c <= a )
assume a is_>=_than {x,y} ; :: thesis: c <= a
then ( a >= x & a >= y ) by YELLOW_0:8;
then a in X ;
hence c <= a by A8, LATTICE3:def 8; :: thesis: verum

end;

hence ex_sup_of {x,y},L by A10, YELLOW_0:15; :: thesis: verum

end;

end;

end;

let D be non empty directed Subset of L; :: according to WAYBEL_3:def 1 :: thesis: ( z <= sup D implies ex d being Element of L st
( d in D & x "\/" y <= d ) )
assume A12: z <= sup D ; :: thesis: ex d being Element of L st
( d in D & x "\/" y <= d )
then consider d1 being Element of L such that
A13: ( d1 in D & x <= d1 ) by A2, Def1;
consider d2 being Element of L such that
A14: ( d2 in D & y <= d2 ) by A4, A12, Def1;
consider d being Element of L such that
A15: ( d in D & d1 <= d & d2 <= d ) by A13, A14, WAYBEL_0:def 1;
A16: ( d in D & x <= d & y <= d ) by A13, A14, A15, ORDERS_2:26;
take d ; :: thesis: ( d in D & x "\/" y <= d )
thus ( d in D & x "\/" y <= d ) by A6, A16, YELLOW_0:18; :: thesis: verum