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 (lower_bound (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 (lower_bound (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 (lower_bound (f,A)) . x >= 0

let A be non empty Subset of X; :: thesis: for x being Element of X holds (lower_bound (f,A)) . x >= 0

let x be Element of X; :: thesis: (lower_bound (f,A)) . x >= 0

then lower_bound ((dist (f,x)) .: A) >= 0 by A2, SEQ_4:43;

hence (lower_bound (f,A)) . x >= 0 by Def3; :: thesis: verum

for A being non empty Subset of X

for x being Element of X holds (lower_bound (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 (lower_bound (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 (lower_bound (f,A)) . x >= 0

let A be non empty Subset of X; :: thesis: for x being Element of X holds (lower_bound (f,A)) . x >= 0

let x be Element of X; :: thesis: (lower_bound (f,A)) . x >= 0

A2: now :: thesis: for rn being Real st rn in (dist (f,x)) .: A holds

rn >= 0

X = dom (dist (f,x))
by FUNCT_2:def 1;rn >= 0

let rn be Real; :: thesis: ( rn in (dist (f,x)) .: A implies rn >= 0 )

assume rn in (dist (f,x)) .: A ; :: thesis: rn >= 0

then consider y being object such that

A3: y in dom (dist (f,x)) and

y in A and

A4: rn = (dist (f,x)) . y by FUNCT_1:def 6;

(dist (f,x)) . y = f . (x,y) by A3, Def2;

hence rn >= 0 by A1, A3, A4, NAGATA_1:29; :: thesis: verum

end;assume rn in (dist (f,x)) .: A ; :: thesis: rn >= 0

then consider y being object such that

A3: y in dom (dist (f,x)) and

y in A and

A4: rn = (dist (f,x)) . y by FUNCT_1:def 6;

(dist (f,x)) . y = f . (x,y) by A3, Def2;

hence rn >= 0 by A1, A3, A4, NAGATA_1:29; :: thesis: verum

then lower_bound ((dist (f,x)) .: A) >= 0 by A2, SEQ_4:43;

hence (lower_bound (f,A)) . x >= 0 by Def3; :: thesis: verum