let u, v be non zero Element of (TOP-REAL 3); :: thesis: for p, q being Element of (ProjectiveSpace (TOP-REAL 3)) st p <> q & p = Dir u & q = Dir v holds
not u <X> v is zero
let p, q be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( p <> q & p = Dir u & q = Dir v implies not u <X> v is zero )
assume A1: ( p <> q & p = Dir u & q = Dir v ) ; :: thesis: not u <X> v is zero
assume u <X> v is zero ; :: thesis: contradiction
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A1, ANPROJ_1:22; :: thesis: verum