let P be Element of absolute ; :: thesis: P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
consider u being non zero Element of (TOP-REAL 3) such that
A1: u . 3 = 1 and
A2: P = Dir u by BKMODEL3:30;
u `3 = 1 by A1, EUCLID_5:def 3;
hence P is non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by A2, Th40; :: thesis: verum