:: deftheorem Def04 defines point_at_infty BKMODEL4:def 4 :
for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( P is point_at_infty iff ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 = 0 ) );