let P be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P in BK_model implies RP3_to_REAL2 P in inside_of_circle (0,0,1) )
assume P in BK_model ; :: thesis: RP3_to_REAL2 P in inside_of_circle (0,0,1)
then reconsider P1 = P as Element of BK_model ;
consider u being non zero Element of (TOP-REAL 3) such that
A1: ( Dir u = P1 & u . 3 = 1 ) and
A2: BK_to_REAL2 P1 = |[(u . 1),(u . 2)]| by BKMODEL2:def 2;
|[(u `1),(u . 2)]| is Element of inside_of_circle (0,0,1) by A2, EUCLID_5:def 1;
then A3: |[(u `1),(u `2)]| is Element of inside_of_circle (0,0,1) by EUCLID_5:def 2;
consider v being non zero Element of (TOP-REAL 3) such that
A4: ( P = Dir v & v `3 = 1 & RP3_to_REAL2 P = |[(v `1),(v `2)]| ) by Def05;
( Dir v = Dir u & u . 3 <> 0 & u . 3 = v . 3 ) by A1, A4, EUCLID_5:def 3;
then u = v by Th16;
hence RP3_to_REAL2 P in inside_of_circle (0,0,1) by A4, A3; :: thesis: verum