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 (((lower_bound pmet,A) . x) - ((lower_bound 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 (((lower_bound pmet,A) . x) - ((lower_bound 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 (((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y)) <= pmet . x,y
A2: pmet is symmetric by A1, NAGATA_1:def 10;
let x, y be Point of T; :: thesis: for A being non empty Subset of T holds abs (((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y)) <= pmet . x,y
let A be non empty Subset of T; :: thesis: abs (((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y)) <= pmet . x,y
A3: for x1, y1 being Point of T holds ((lower_bound pmet,A) . y1) - ((lower_bound pmet,A) . x1) >= - (pmet . x1,y1)

proof

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

proof

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

end;

( not (dist pmet,y1) .: A is empty & (dist pmet,y1) .: A is bounded_below ) by A1, Lm1;
then (lower_bound ((dist pmet,y1) .: A)) - 0 >= (lower_bound ((dist pmet,x1) .: A)) - (pmet . x1,y1) by A5, SEQ_4:60;
then A11: (lower_bound ((dist pmet,y1) .: A)) - (lower_bound ((dist pmet,x1) .: A)) >= 0 - (pmet . x1,y1) by XREAL_1:19;
lower_bound ((dist pmet,y1) .: A) = (lower_bound pmet,A) . y1 by Def3;
hence ((lower_bound pmet,A) . y1) - ((lower_bound pmet,A) . x1) >= - (pmet . x1,y1) by A11, Def3; :: thesis: verum

end;

then ((lower_bound pmet,A) . y) - ((lower_bound pmet,A) . x) >= - (pmet . x,y) ;
then - (((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y)) >= - (pmet . x,y) ;
then A12: ((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y) <= pmet . x,y by XREAL_1:26;
((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y) >= - (pmet . y,x) by A3;
then ((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y) >= - (pmet . x,y) by A2, METRIC_1:def 5;
hence abs (((lower_bound pmet,A) . x) - ((lower_bound pmet,A) . y)) <= pmet . x,y by A12, ABSVALUE:12; :: thesis: verum