MetricSpaceNorm (REAL-NS n) = Euclid n by Th15;
hence Euclid n is complete ; :: thesis: verum