reconsider M = MetrStruct(# REAL ,real_dist #) as non empty MetrStruct ;
M is MetrSpace

proof

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 M is MetrSpace by Th6; :: thesis: verum

end;

hence ( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle ) ; :: thesis: verum