theorem Th4: :: EUCLID_5:4

0. (TOP-REAL 3) = |[0,0,0]|