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
(inf 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
(inf 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
(inf f,A) . x = 0
let A be Subset of X; :: thesis: for x being Element of X st x in A holds
(inf f,A) . x = 0
let x be Element of X; :: thesis: ( x in A implies (inf f,A) . x = 0 )
assume A2: x in A ; :: thesis: (inf f,A) . x = 0
then reconsider A = A as non empty Subset of X ;
f is Reflexive by A1, NAGATA_1:def 10;
then ( f . x,x = 0 & X = dom (dist f,x) ) by FUNCT_2:def 1, METRIC_1:def 3;
then ( (dist f,x) . x = 0 & x in dom (dist f,x) ) by Def2;
then ( 0 in (dist f,x) .: A & not (dist f,x) .: A is empty & (dist f,x) .: A is bounded_below ) by A1, A2, Lm1, FUNCT_1:def 12;
then ( inf ((dist f,x) .: A) <= 0 & f is bounded_below ) by A1, Lm1, SEQ_4:def 5;
then ( (inf f,A) . x <= 0 & (inf f,A) . x >= 0 ) by A1, Def3, Th5;
hence (inf f,A) . x = 0 ; :: thesis: verum