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 )

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

hereby :: thesis: ( ( for X being non empty directed Subset of L holds ex_sup_of X,L ) implies L is up-complete )

assume A7:
for X being non empty directed Subset of L holds ex_sup_of X,L
; :: thesis: 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

end;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 b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or x <= b_{1} ) ) & ( for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ex b_{2} being Element of the carrier of L st

( X is_<=_than b_{2} & not b_{1} <= b_{2} ) or b_{1} = 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 b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ex b_{2} being Element of the carrier of L st

( X is_<=_than b_{2} & not b_{1} <= b_{2} ) or b_{1} = x )

let c be Element of L; :: thesis: ( not X is_<=_than c or ex b_{1} being Element of the carrier of L st

( X is_<=_than b_{1} & not c <= b_{1} ) 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;( not X is_<=_than b

( not X is_<=_than b

( X is_<=_than b

thus ( X is_<=_than x & ( for b being Element of L st X is_<=_than b holds

b >= x ) ) by A2, A3; :: thesis: for b

( not X is_<=_than b

( X is_<=_than b

let c be Element of L; :: thesis: ( not X is_<=_than c or ex b

( X is_<=_than b

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

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