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_metric_of the carrier of T holds
min r,m is_metric_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_metric_of the carrier of T holds
min r,m is_metric_of the carrier of T
let m be Function of [:the carrier of T,the carrier of T:], REAL ; :: thesis: ( r > 0 & m is_metric_of the carrier of T implies min r,m is_metric_of the carrier of T )
assume that
A1: r > 0 and
A2: m is_metric_of the carrier of T ; :: thesis: min r,m is_metric_of the carrier of T
for a, b, c being Element of T holds
( m . a,a = 0 & m . a,b = m . b,a & m . a,c <= (m . a,b) + (m . b,c) ) by A2, PCOMPS_1:def 7;
then m is_a_pseudometric_of the carrier of T by Lm8;
then A3: min r,m is_a_pseudometric_of the carrier of T by A1, Th30;
let a, b, c be Element of T; :: according to PCOMPS_1:def 7 :: thesis: ( ( not (min r,m) . a,b = 0 or a = b ) & ( not a = b or (min r,m) . a,b = 0 ) & (min r,m) . a,b = (min r,m) . b,a & (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . b,c) )
thus ( (min r,m) . a,b = 0 iff a = b ) :: thesis: ( (min r,m) . a,b = (min r,m) . b,a & (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . b,c) )

proof

( (min r,m) . a,b = 0 implies a = b )

proof

assume (min r,m) . a,b = 0 ; :: thesis: a = b
then min r,(m . a,b) = 0 by Lm9;
then m . a,b = 0 by A1, XXREAL_0:def 9;
hence a = b by A2, PCOMPS_1:def 7; :: thesis: verum

end;

hence ( (min r,m) . a,b = 0 iff a = b ) by A3, Lm8; :: thesis: verum

end;

thus ( (min r,m) . a,b = (min r,m) . b,a & (min r,m) . a,c <= ((min r,m) . a,b) + ((min r,m) . b,c) ) by A3, Lm8; :: thesis: verum