theorem Th61: :: BKMODEL4:71

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