let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: Dir (dir2a P) <> Dir (dir2b P)
assume Dir (dir2a P) = Dir (dir2b P) ; :: thesis: contradiction
then are_Prop dir2a P, dir2b P by ANPROJ_1:22;
then consider a being Real such that
A1: a <> 0 and
A2: dir2a P = a * (dir2b P) by ANPROJ_1:1;
0 = (dir2a P) `3 by EUCLID_5:2
.= a * ((dir2b P) `3) by A2, RVSUM_1:44
.= a * 1 by EUCLID_5:2 ;
hence contradiction by A1; :: thesis: verum