reconsider P = Dir |[1,0,1]| as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u `3 <> 0

proof

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

end;

hence Dir |[1,0,1]| is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by Def04; :: thesis: verum