let L be non empty reflexive antisymmetric RelStr ; :: thesis: ( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )
hereby :: thesis: ( ( for X being non empty directed Subset of L holds ex_sup_of X,L ) implies L is up-complete )
assume A1: L is up-complete ; :: thesis: for X being non empty directed Subset of L holds ex_sup_of X,L
let X be non empty directed Subset of L; :: thesis: ex_sup_of X,L
consider x being Element of L such that
A2: x is_>=_than X and
A3: for y being Element of L st y is_>=_than X holds
x <= y by A1;
thus ex_sup_of X,L :: thesis: verum
proof
take x ; :: according to YELLOW_0:def 7 :: thesis: ( X is_<=_than x & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or x <= b1 ) ) & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = x ) ) )
thus ( X is_<=_than x & ( for b being Element of L st X is_<=_than b holds
b >= x ) ) by A2, A3; :: thesis: for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = x )
let c be Element of L; :: thesis: ( not X is_<=_than c or ex b1 being Element of the carrier of L st
( X is_<=_than b1 & not c <= b1 ) or c = x )
assume that
A4: X is_<=_than c and
A5: for b being Element of L st X is_<=_than b holds
b >= c ; :: thesis: c = x
A6: c <= x by A2, A5;
c >= x by A3, A4;
hence c = x by A6, ORDERS_2:2; :: thesis: verum
end;
end;
assume A7: for X being non empty directed Subset of L holds ex_sup_of X,L ; :: thesis: L is up-complete
let X be non empty directed Subset of L; :: according to WAYBEL_0:def 39 :: thesis: ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) )
ex_sup_of X,L by A7;
then ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) holds
c = a ) ) ;
hence ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) ; :: thesis: verum