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 )

hereby :: thesis: ( ( for X being non empty Subset of L holds ex_inf_of X,L ) implies 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

proof

take x ; :: according to YELLOW_0:def 8 :: thesis: ( x is_<=_than X & ( for b₁ being Element of the carrier of L holds
( not b₁ is_<=_than X or b₁ <= x ) ) & ( for b₁ being Element of the carrier of L holds
( not b₁ is_<=_than X or ex b₂ being Element of the carrier of L st
( b₂ is_<=_than X & not b₂ <= b₁ ) or b₁ = 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₁ being Element of the carrier of L holds
( not b₁ is_<=_than X or ex b₂ being Element of the carrier of L st
( b₂ is_<=_than X & not b₂ <= b₁ ) or b₁ = x )
let c be Element of L; :: thesis: ( not c is_<=_than X or ex b₁ being Element of the carrier of L st
( b₁ is_<=_than X & not b₁ <= 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;

end;

assume A7: for X being non empty Subset of L holds ex_inf_of X,L ; :: thesis: L is /\-complete
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