let T be non empty TopSpace; :: thesis: for pmet being Function of [:the carrier of T,the carrier of T:], REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y
let pmet be Function of [:the carrier of T,the carrier of T:], REAL ; :: thesis: ( pmet is_a_pseudometric_of the carrier of T implies for x, y being Point of T
for A being non empty Subset of T holds abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y )
assume A1: pmet is_a_pseudometric_of the carrier of T ; :: thesis: for x, y being Point of T
for A being non empty Subset of T holds abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y
let x, y be Point of T; :: thesis: for A being non empty Subset of T holds abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y
let A be non empty Subset of T; :: thesis: abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y
for x1, y1 being Point of T holds ((inf pmet,A) . y1) - ((inf pmet,A) . x1) >= - (pmet . x1,y1)

proof

let x1, y1 be Point of T; :: thesis: ((inf pmet,A) . y1) - ((inf pmet,A) . x1) >= - (pmet . x1,y1)
A2: ( not (dist pmet,x1) .: A is empty & (dist pmet,x1) .: A is bounded_below & not (dist pmet,y1) .: A is empty & (dist pmet,y1) .: A is bounded_below & pmet is bounded_below ) by A1, Lm1;
for rn being real number st rn in (dist pmet,y1) .: A holds
rn >= (inf ((dist pmet,x1) .: A)) - (pmet . x1,y1)

proof

let rn be real number ; :: thesis: ( rn in (dist pmet,y1) .: A implies rn >= (inf ((dist pmet,x1) .: A)) - (pmet . x1,y1) )
assume rn in (dist pmet,y1) .: A ; :: thesis: rn >= (inf ((dist pmet,x1) .: A)) - (pmet . x1,y1)
then consider z being set such that
A3: ( z in dom (dist pmet,y1) & z in A & (dist pmet,y1) . z = rn ) by FUNCT_1:def 12;
reconsider z = z as Point of T by A3;
dom (dist pmet,x1) = the carrier of T by FUNCT_2:def 1;
then ( pmet is triangle & (dist pmet,x1) . z in (dist pmet,x1) .: A & (dist pmet,x1) . z = pmet . x1,z ) by A1, A3, Def2, FUNCT_1:def 12, NAGATA_1:def 10;
then ( (pmet . x1,y1) + (pmet . y1,z) >= pmet . x1,z & pmet . x1,z >= inf ((dist pmet,x1) .: A) ) by A2, METRIC_1:def 6, SEQ_4:def 5;
then (pmet . x1,y1) + (pmet . y1,z) >= (inf ((dist pmet,x1) .: A)) + 0 by XXREAL_0:2;
then (pmet . y1,z) - 0 >= (inf ((dist pmet,x1) .: A)) - (pmet . x1,y1) by XREAL_1:23;
hence rn >= (inf ((dist pmet,x1) .: A)) - (pmet . x1,y1) by A3, Def2; :: thesis: verum

end;

then (inf ((dist pmet,y1) .: A)) - 0 >= (inf ((dist pmet,x1) .: A)) - (pmet . x1,y1) by A2, SEQ_4:60;
then ( (inf ((dist pmet,y1) .: A)) - (inf ((dist pmet,x1) .: A)) >= 0 - (pmet . x1,y1) & inf ((dist pmet,y1) .: A) = (inf pmet,A) . y1 ) by Def3, XREAL_1:19;
hence ((inf pmet,A) . y1) - ((inf pmet,A) . x1) >= - (pmet . x1,y1) by Def3; :: thesis: verum

end;

then ( ((inf pmet,A) . y) - ((inf pmet,A) . x) >= - (pmet . x,y) & ((inf pmet,A) . x) - ((inf pmet,A) . y) >= - (pmet . y,x) & pmet is symmetric ) by A1, NAGATA_1:def 10;
then ( - (((inf pmet,A) . x) - ((inf pmet,A) . y)) >= - (pmet . x,y) & ((inf pmet,A) . x) - ((inf pmet,A) . y) >= - (pmet . x,y) ) by METRIC_1:def 5;
then ( ((inf pmet,A) . x) - ((inf pmet,A) . y) <= pmet . x,y & ((inf pmet,A) . x) - ((inf pmet,A) . y) >= - (pmet . x,y) ) by XREAL_1:26;
hence abs (((inf pmet,A) . x) - ((inf pmet,A) . y)) <= pmet . x,y by ABSVALUE:12; :: thesis: verum