let X be non empty set ; 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; ( 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
; 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; for x being Element of X holds (lower_bound (f,A)) . x >= 0
let x be Element of X; (lower_bound (f,A)) . x >= 0
A2:
now for rn being Real st rn in (dist (f,x)) .: A holds
rn >= 0 let rn be
Real;
( rn in (dist (f,x)) .: A implies rn >= 0 )assume
rn in (dist (f,x)) .: A
;
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;
verum end;
X = dom (dist (f,x))
by FUNCT_2:def 1;
then
lower_bound ((dist (f,x)) .: A) >= 0
by A2, SEQ_4:43;
hence
(lower_bound (f,A)) . x >= 0
by Def3; verum