let P, Q be Element of BK_model ; :: thesis: ( P = Q iff BK_to_REAL2 P = BK_to_REAL2 Q )
thus ( P = Q implies BK_to_REAL2 P = BK_to_REAL2 Q ) ; :: thesis: ( BK_to_REAL2 P = BK_to_REAL2 Q implies P = Q )
assume A1: BK_to_REAL2 P = BK_to_REAL2 Q ; :: thesis: P = Q
consider u being non zero Element of (TOP-REAL 3) such that
A2: ( Dir u = P & u . 3 = 1 & BK_to_REAL2 P = |[(u . 1),(u . 2)]| ) by Def01;
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 Def01;
( u . 1 = v . 1 & u . 2 = v . 2 & u . 3 = v . 3 ) by A1, A2, A3, FINSEQ_1:77;
then ( u `1 = v . 1 & u `2 = v . 2 & u `3 = v . 3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A4: ( u `1 = v `1 & u `2 = v `2 & u `3 = v `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
( u = |[(u `1),(u `2),(u `3)]| & v = |[(v `1),(v `2),(v `3)]| ) by EUCLID_5:3;
hence P = Q by A2, A3, A4; :: thesis: verum