let T be non empty TopSpace; :: thesis: for r being Real
for m being Function of [:the carrier of T,the carrier of T:],REAL st r > 0 & m is_a_pseudometric_of the carrier of T holds
min r,m is_a_pseudometric_of the carrier of T
let r be Real; :: thesis: for m being Function of [:the carrier of T,the carrier of T:],REAL st r > 0 & m is_a_pseudometric_of the carrier of T holds
min r,m is_a_pseudometric_of the carrier of T
let m be Function of [:the carrier of T,the carrier of T:],REAL ; :: thesis: ( r > 0 & m is_a_pseudometric_of the carrier of T implies min r,m is_a_pseudometric_of the carrier of T )
assume that
A1: r > 0 and
A2: m is_a_pseudometric_of the carrier of T ; :: thesis: min r,m is_a_pseudometric_of the carrier of T

now

let a, b, c be Element of T; :: thesis: ( (min r,m) . a,a = 0 & (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b) )
m . a,a = 0 by A2, Th28;
then min r,(m . a,a) = 0 by A1, XXREAL_0:def 9;
hence (min r,m) . a,a = 0 by Lm9; :: thesis: (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b)
thus (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b) :: thesis: verum

proof

now

per cases ( ((min r,m) . a,b) + ((min r,m) . c,b) >= r or ((min r,m) . a,b) + ((min r,m) . c,b) < r ) ;

suppose A3: ((min r,m) . a,b) + ((min r,m) . c,b) >= r ; :: thesis: (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b)

min r,(m . a,c) <= r by XXREAL_0:17;
then (min r,m) . a,c <= r by Lm9;
hence (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b) by A3, XXREAL_0:2; :: thesis: verum

end;

suppose A4: ((min r,m) . a,b) + ((min r,m) . c,b) < r ; :: thesis: (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b)

m . c,b >= 0 by A2, Th29;
then 0 <= min r,(m . c,b) by A1, XXREAL_0:20;
then A5: 0 <= (min r,m) . c,b by Lm9;
m . a,b >= 0 by A2, Th29;
then 0 <= min r,(m . a,b) by A1, XXREAL_0:20;
then A6: 0 <= (min r,m) . a,b by Lm9;
then (min r,m) . a,b < r by A4, A5, Lm1;
then min r,(m . a,b) < r by Lm9;
then min r,(m . a,b) = m . a,b by XXREAL_0:def 9;
then A7: (min r,m) . a,b = m . a,b by Lm9;
(min r,m) . c,b < r by A4, A6, A5, Lm1;
then min r,(m . c,b) < r by Lm9;
then min r,(m . c,b) = m . c,b by XXREAL_0:def 9;
then A8: (min r,m) . c,b = m . c,b by Lm9;
( min r,(m . a,c) <= m . a,c & m . a,c <= (m . a,b) + (m . c,b) ) by A2, Th28, XXREAL_0:17;
then min r,(m . a,c) <= (m . a,b) + (m . c,b) by XXREAL_0:2;
hence (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b) by A7, A8, Lm9; :: thesis: verum

end;

end;

end;

hence (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . c,b) ; :: thesis: verum

end;

end;

hence min r,m is_a_pseudometric_of the carrier of T by Th28; :: thesis: verum