theorem :: EUCLID_2:34

for n being Nat holds |((0. (TOP-REAL n)),(0. (TOP-REAL n)))| = 0 by Th30;