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