let P be Element of BK_model ; :: thesis: REAL2_to_BK (BK_to_REAL2 P) = P
consider u being non zero Element of (TOP-REAL 3) such that
A1: Dir u = P and
A2: u . 3 = 1 and
A3: BK_to_REAL2 P = |[(u . 1),(u . 2)]| by Def01;
consider Q being Element of (TOP-REAL 2) such that
A4: Q = BK_to_REAL2 P and
A5: REAL2_to_BK (BK_to_REAL2 P) = Dir |[(Q `1),(Q `2),1]| by Def02;
A6: not |[(Q `1),(Q `2),1]| is zero by EUCLID_5:4, FINSEQ_1:78;
are_Prop |[(Q `1),(Q `2),1]|,u

proof

A7: ( Q `1 = u . 1 & Q `2 = u . 2 ) by A3, A4, EUCLID:52;
u = |[(u `1),(u `2),(u `3)]| by EUCLID_5:3
.= |[(u . 1),(u `2),(u `3)]| by EUCLID_5:def 1
.= |[(u . 1),(u . 2),(u `3)]| by EUCLID_5:def 2
.= |[(u . 1),(u . 2),(u . 3)]| by EUCLID_5:def 3 ;
hence are_Prop |[(Q `1),(Q `2),1]|,u by A2, A7; :: thesis: verum

end;

hence REAL2_to_BK (BK_to_REAL2 P) = P by A1, A5, A6, ANPROJ_1:22; :: thesis: verum