reconsider u = |[0,0,1]| as non zero Element of (TOP-REAL 3) ;
reconsider P = Dir u as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
take P ; :: thesis: not P is point_at_infty

now :: thesis: for v being non zero Element of (TOP-REAL 3) st P = Dir v holds
v `3 <> 0

let v be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir v implies v `3 <> 0 )
assume P = Dir v ; :: thesis: v `3 <> 0
then are_Prop u,v by ANPROJ_1:22;
then consider a being Real such that
A1: a <> 0 and
A2: v = a * u by ANPROJ_1:1;
v `3 = a * (u `3) by A2, EUCLID_5:9
.= a * 1 by EUCLID_5:2
.= a ;
hence v `3 <> 0 by A1; :: thesis: verum

end;

hence not P is point_at_infty ; :: thesis: verum