let P be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P in absolute implies RP3_to_REAL2 P in circle (0,0,1) )
assume A1: P in absolute ; :: thesis: RP3_to_REAL2 P in circle (0,0,1)
consider u being non zero Element of (TOP-REAL 3) such that
A2: ( P = Dir u & u `3 = 1 & RP3_to_REAL2 P = |[(u `1),(u `2)]| ) by Def05;
u . 3 = 1 by A2, EUCLID_5:def 3;
then |[(u . 1),(u . 2)]| in circle (0,0,1) by A1, A2, BKMODEL1:84;
then |[(u `1),(u . 2)]| in circle (0,0,1) by EUCLID_5:def 1;
hence RP3_to_REAL2 P in circle (0,0,1) by A2, EUCLID_5:def 2; :: thesis: verum