reconsider M = MetrStruct(# REAL,real_dist #) as non empty MetrStruct ;
for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) by Th8, Th9, Th10;
hence ( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle ) by Th6; :: thesis: verum