consider u being Element of (TOP-REAL 3) such that
A1: not u is zero and
A2: P = Dir u by ANPROJ_1:26;
u . 3 <> 0 by A1, A2, Th67;
then A3: u `3 <> 0 by EUCLID_5:def 3;
then reconsider r = 1 / (u `3) as non zero Real ;
reconsider v = |[((u `1) / (u `3)),((u `2) / (u `3)),1]| as non zero Element of (TOP-REAL 3) by Th36;
r * u = (1 / (u `3)) * |[(u `1),(u `2),(u `3)]| by EUCLID_5:3
.= |[((1 / (u `3)) * (u `1)),((1 / (u `3)) * (u `2)),((1 / (u `3)) * (u `3))]| by EUCLID_5:8
.= |[((u `1) / (u `3)),((1 / (u `3)) * (u `2)),((1 / (u `3)) * (u `3))]| by XCMPLX_1:99
.= |[((u `1) / (u `3)),((u `2) / (u `3)),((1 / (u `3)) * (u `3))]| by XCMPLX_1:99
.= |[((u `1) / (u `3)),((u `2) / (u `3)),((u `3) / (u `3))]| by XCMPLX_1:99
.= v by A3, XCMPLX_1:60 ;
then are_Prop u,v by ANPROJ_1:1;
then A4: P = Dir v by A1, A2, ANPROJ_1:22;
A5: v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
then |[(v . 1),(v . 2)]| in circle (0,0,1) by A4, Th68;
hence ex b₁ being Element of circle (0,0,1) ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & b₁ = |[(u . 1),(u . 2)]| ) by A4, A5; :: thesis: verum