let P be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); ( P in absolute implies RP3_to_REAL2 P in circle (0,0,1) )
assume A1:
P in absolute
; 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; verum