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))

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

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

then
((lower_bound (pmet,A)) . y) - ((lower_bound (pmet,A)) . x) >= - (pmet . (x,y))
;
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))

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;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

( not (dist (pmet,y1)) .: A is empty & (dist (pmet,y1)) .: A is bounded_below )
by A1, Lm1;
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;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

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

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