theorem Th18: :: EUCLID:21

for n being Nat holds Pitag_dist n is_metric_of REAL n