let T be non empty TopSpace; 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; 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; ( 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
; min (r,m) is_metric_of the carrier of T
let a, b, c be Element of T; PCOMPS_1:def 6 ( ( 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)) )
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;
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;
( (min (r,m)) . (a,b) = 0 implies a = b )
hence
( (min (r,m)) . (a,b) = 0 iff a = b )
by A3, Lm8; ( (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) = (min (r,m)) . (b,a) & (min (r,m)) . (a,c) <= ((min (r,m)) . (a,b)) + ((min (r,m)) . (b,c)) )
by A3, Lm8; verum