consider u being Element of (TOP-REAL 3) such that
A1: not u is zero and
A2: P = Dir u by ANPROJ_1:26;
A3: not P is point_at_infty ;
reconsider v = |[((u `1) / (u `3)),((u `2) / (u `3)),1]| as non zero Element of (TOP-REAL 3) ;
(u `3) * v = |[((u `3) * ((u `1) / (u `3))),((u `3) * ((u `2) / (u `3))),((u `3) * 1)]| by EUCLID_5:8
.= |[(u `1),((u `3) * ((u `2) / (u `3))),(u `3)]| by A1, A2, A3, XCMPLX_1:87
.= |[(u `1),(u `2),(u `3)]| by A1, A2, A3, XCMPLX_1:87
.= u by EUCLID_5:3 ;
then are_Prop u,v by A1, A2, A3, ANPROJ_1:1;
then A4: P = Dir v by A2, A1, ANPROJ_1:22;
A5: v `3 = 1 by EUCLID_5:2;
|[(v `1),(v `2)]| is Element of REAL 2 by EUCLID:22;
hence ex b<sub>1</sub> being Element of REAL 2 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