consider u being non zero Element of (TOP-REAL 3) such that
A1: ((u . 1) ^2) + ((u . 2) ^2) = 1 and
A2: u . 3 = 1 and
A3: P = Dir u by BKMODEL1:89;
Dir |[(- (u . 2)),(u . 1),0]| is Element of real_projective_plane by A1, BKMODEL1:91, ANPROJ_1:26;
hence ex b₁ being Element of real_projective_plane ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & b₁ = Dir |[(- (u . 2)),(u . 1),0]| ) by A1, A2, A3; :: thesis: verum