consider u being Element of (TOP-REAL 3) such that
A2: ( not u is zero & p = Dir u ) by ANPROJ_1:26;
consider v being Element of (TOP-REAL 3) such that
A3: ( not v is zero & q = Dir v ) by ANPROJ_1:26;
reconsider u = u, v = v as non zero Element of (TOP-REAL 3) by A2, A3;
not u <X> v is zero by A1, A2, A3, Th64;
then Dir (u <X> v) is Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
hence ex b₁ being Point of real_projective_plane ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & b₁ = Dir (u <X> v) ) by A2, A3; :: thesis: verum