let L be non empty reflexive antisymmetric RelStr ; :: thesis:

hereby :: thesis:

assume A1: L is /\-complete ; :: thesis:
let X be non empty Subset of L; :: thesis:
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:

proof

take x ; :: according to YELLOW_0:def 8 :: thesis:
thus ( X is_>=_than x & ( for b being Element of L st X is_>=_than b holds
b <= x ) ) by A2, A3; :: thesis:
let c be Element of L; :: thesis:
assume that
A4: X is_>=_than c and
A5: for b being Element of L st X is_>=_than b holds
b <= c ; :: thesis:
A6: c <= x by A3, A4;
c >= x by A2, A5;
hence c = x by A6, ORDERS_2:2; :: thesis:

end;

end;

assume A7: for X being non empty Subset of L holds ex_inf_of X,L ; :: thesis:
let X be non empty Subset of L; :: according to WAYBEL_0:def 40 :: thesis:
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: