let X be non empty set ; :: thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being non empty Subset of X
for x being Element of X holds (inf f,A) . x >= 0
let f be Function of [:X,X:],REAL ; :: thesis: ( f is_a_pseudometric_of X implies for A being non empty Subset of X
for x being Element of X holds (inf f,A) . x >= 0 )
assume A1: f is_a_pseudometric_of X ; :: thesis: for A being non empty Subset of X
for x being Element of X holds (inf f,A) . x >= 0
let A be non empty Subset of X; :: thesis: for x being Element of X holds (inf f,A) . x >= 0
let x be Element of X; :: thesis: (inf f,A) . x >= 0
consider a being set such that
A2: a in A by XBOOLE_0:def 1;
( a in X & X = dom (dist f,x) ) by A2, FUNCT_2:def 1;
then A3: (dist f,x) . a in (dist f,x) .: A by A2, FUNCT_1:def 12;

now

let rn be real number ; :: thesis: ( rn in (dist f,x) .: A implies rn >= 0 )
assume rn in (dist f,x) .: A ; :: thesis: rn >= 0
then consider y being set such that
A4: ( y in dom (dist f,x) & y in A & rn = (dist f,x) . y ) by FUNCT_1:def 12;
(dist f,x) . y = f . x,y by A4, Def2;
hence rn >= 0 by A1, A4, NAGATA_1:29; :: thesis: verum

end;

then ( inf ((dist f,x) .: A) >= 0 & f is bounded_below ) by A1, A3, Lm1, SEQ_4:60;
hence (inf f,A) . x >= 0 by Def3; :: thesis: verum