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 by Th1;
assume A4: z >> y ; :: thesis: ( ex_sup_of {x,y},L & x "\/" y << z )
then A5: z >= y by Th1;
hereby :: thesis: x "\/" y << z
per cases ( L is with_suprema or L is /\-complete ) by A1;
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 object ; :: 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 ;
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 :: thesis: for a being Element of L st a is_>=_than {x,y} holds
c <= a
let a be Element of L; :: thesis: ( a is_>=_than {x,y} implies c <= a )
assume A12: a is_>=_than {x,y} ; :: thesis: c <= a
then A13: a >= x by YELLOW_0:8;
a >= y by A12, YELLOW_0:8;
then a in X by A13;
hence c <= a by A8; :: 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 A14: 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
A15: d1 in D and
A16: x <= d1 by A2;
consider d2 being Element of L such that
A17: d2 in D and
A18: y <= d2 by A4, A14;
consider d being Element of L such that
A19: d in D and
A20: d1 <= d and
A21: d2 <= d by A15, A17, WAYBEL_0:def 1;
A22: x <= d by A16, A20, ORDERS_2:3;
A23: y <= d by A18, A21, ORDERS_2:3;
take d ; :: thesis: ( d in D & x "\/" y <= d )
thus ( d in D & x "\/" y <= d ) by A6, A19, A22, A23, YELLOW_0:18; :: thesis: verum