:: deftheorem defines # CARDFIL3:def 3 :
for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds # x = x;