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 Subset of X

for x being Element of X st x in A 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 Subset of X

for x being Element of X st x in A holds

(lower_bound (f,A)) . x = 0 )

assume A1: f is_a_pseudometric_of X ; :: thesis: for A being Subset of X

for x being Element of X st x in A holds

(lower_bound (f,A)) . x = 0

let A be Subset of X; :: thesis: for x being Element of X st x in A holds

(lower_bound (f,A)) . x = 0

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

assume A2: x in A ; :: thesis: (lower_bound (f,A)) . x = 0

then reconsider A = A as non empty Subset of X ;

A3: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A1, Lm1;

f is Reflexive by A1, NAGATA_1:def 10;

then f . (x,x) = 0 by METRIC_1:def 2;

then ( X = dom (dist (f,x)) & (dist (f,x)) . x = 0 ) by Def2, FUNCT_2:def 1;

then 0 in (dist (f,x)) .: A by A2, FUNCT_1:def 6;

then lower_bound ((dist (f,x)) .: A) <= 0 by A3, SEQ_4:def 2;

then (lower_bound (f,A)) . x <= 0 by Def3;

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

for A being Subset of X

for x being Element of X st x in A 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 Subset of X

for x being Element of X st x in A holds

(lower_bound (f,A)) . x = 0 )

assume A1: f is_a_pseudometric_of X ; :: thesis: for A being Subset of X

for x being Element of X st x in A holds

(lower_bound (f,A)) . x = 0

let A be Subset of X; :: thesis: for x being Element of X st x in A holds

(lower_bound (f,A)) . x = 0

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

assume A2: x in A ; :: thesis: (lower_bound (f,A)) . x = 0

then reconsider A = A as non empty Subset of X ;

A3: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A1, Lm1;

f is Reflexive by A1, NAGATA_1:def 10;

then f . (x,x) = 0 by METRIC_1:def 2;

then ( X = dom (dist (f,x)) & (dist (f,x)) . x = 0 ) by Def2, FUNCT_2:def 1;

then 0 in (dist (f,x)) .: A by A2, FUNCT_1:def 6;

then lower_bound ((dist (f,x)) .: A) <= 0 by A3, SEQ_4:def 2;

then (lower_bound (f,A)) . x <= 0 by Def3;

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