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