let P be Element of BK_model ; :: thesis: P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
reconsider p = P as Element of (ProjectiveSpace (TOP-REAL 3)) ;
consider u being Element of (TOP-REAL 3) such that
P1: not u is zero and
P2: p = Dir u by ANPROJ_1:26;
u . 3 <> 0 by P1, P2, BKMODEL2:2;
then u `3 <> 0 by EUCLID_5:def 3;
hence P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by P1, P2, Th40; :: thesis: verum