let X be non empty set ; :: thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) ) )
let f be Function of [:X,X:],REAL ; :: thesis: ( f is_a_pseudometric_of X implies ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) ) ) )
assume A1: f is_a_pseudometric_of X ; :: thesis: ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) ) )

A2: now

let A be non empty Subset of X; :: thesis: for x being Element of X holds
( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below )
let x be Element of X; :: thesis: ( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below )
consider a being set such that
A3: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of X by A3;
A4: 0 is LowerBound of (dist f,x) .: A

proof

let rn be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not rn in (dist f,x) .: A or 0 <= rn )
assume rn in (dist f,x) .: A ; :: thesis: 0 <= rn
then consider y being set such that
A5: y in dom (dist f,x) and
y in A and
A6: rn = (dist f,x) . y by FUNCT_1:def 12;
reconsider y = y as Element of X by A5;
f . x,y >= 0 by A1, NAGATA_1:29;
hence rn >= 0 by A6, Def2; :: thesis: verum

end;

dom (dist f,x) = X by FUNCT_2:def 1;
hence ( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) by A4, XXREAL_2:def 9; :: thesis: verum

end;

now

let xy be set ; :: thesis: ( xy in dom f implies f . xy > - 1 )
assume xy in dom f ; :: thesis: f . xy > - 1
then consider x, y being set such that
A7: ( x in X & y in X ) and
A8: [x,y] = xy by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of X by A7;
( f . x,y >= 0 & 0 > - 1 ) by A1, NAGATA_1:29;
hence f . xy > - 1 by A8; :: thesis: verum

end;

hence ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) ) ) by A2, SEQ_2:def 2; :: thesis: verum