let L be non empty reflexive antisymmetric RelStr ; :: thesis: ( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )

let X be non empty Subset of L; :: according to WAYBEL_0:def 40 :: 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_inf_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 Subset of L holds ex_inf_of X,L ) implies L is /\-complete )

assume A7:
for X being non empty Subset of L holds ex_inf_of X,L
; :: thesis: L is /\-complete assume A1:
L is /\-complete
; :: thesis: for X being non empty Subset of L holds ex_inf_of X,L

let X be non empty Subset of L; :: thesis: ex_inf_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_inf_of X,L :: thesis: verum

end;let X be non empty Subset of L; :: thesis: ex_inf_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_inf_of X,L :: thesis: verum

proof

take
x
; :: according to YELLOW_0:def 8 :: thesis: ( x is_<=_than X & ( for b_{1} being Element of the carrier of L holds

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

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

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

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

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

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

c >= x by A2, A5;

hence c = x by A6, ORDERS_2:2; :: thesis: verum

end;( not b

( not b

( 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 b

( b

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

( 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 A3, A4;

c >= x by A2, A5;

hence c = x by A6, ORDERS_2:2; :: thesis: verum

let X be non empty Subset of L; :: according to WAYBEL_0:def 40 :: 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_inf_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