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