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 |.(((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 |.(((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 |.(((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 |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
let A be non empty Subset of T; :: thesis: |.(((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 st rn in (dist (pmet,y1)) .: A holds
rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))

proof

let rn be Real; :: 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 object 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 6;
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 5;
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 6;
then pmet . (x1,z) >= lower_bound ((dist (pmet,x1)) .: A) by A4, A9, SEQ_4:def 2;
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:21;
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:43;
then A11: (lower_bound ((dist (pmet,y1)) .: A)) - (lower_bound ((dist (pmet,x1)) .: A)) >= 0 - (pmet . (x1,y1)) by XREAL_1:17;
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:24;
((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 4;
hence |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y) by A12, ABSVALUE:5; :: thesis: verum