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 Th9, Th10, Th11;
hence ( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle ) by Th6; :: thesis: verum