:: deftheorem NGDef defines naturally_generated GTARSKI1:def 15 :
for M being MetrTarskiStr holds
( M is naturally_generated iff ( ( for a, b, c being POINT of M holds
( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds
( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) ) );