reconsider u = |[1,0,0]| 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: P is point_at_infty
u `3 = 0 by EUCLID_5:2;
hence P is point_at_infty ; :: thesis: verum