let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 <> 0 ) implies not P is point_at_infty )
given u being non zero Element of (TOP-REAL 3) such that A1: P = Dir u and
A2: u `3 <> 0 ; :: 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 A1, ANPROJ_1:22;
then consider a being Real such that
A3: a <> 0 and
A4: v = a * u by ANPROJ_1:1;
v `3 = a * (u `3) by A4, EUCLID_5:9;
hence v `3 <> 0 by A2, A3; :: thesis: verum
end;
hence not P is point_at_infty ; :: thesis: verum