theorem Th62: :: BKMODEL4:72

for P being Element of absolute holds P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))