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