assume A1: ( Dir100 = Dir010 or Dir100 = Dir001 or Dir100 = Dir111 or Dir010 = Dir001 or Dir010 = Dir111 or Dir001 = Dir111 ) ; :: thesis: contradiction
consider u100 being Element of (TOP-REAL 3) such that
A2: u100 = |[1,0,0]| and
A3: Dir100 = Dir u100 ;
consider u010 being Element of (TOP-REAL 3) such that
A4: u010 = |[0,1,0]| and
A5: Dir010 = Dir u010 ;
consider u001 being Element of (TOP-REAL 3) such that
A6: u001 = |[0,0,1]| and
A7: Dir001 = Dir u001 ;
consider u111 being Element of (TOP-REAL 3) such that
A8: u111 = |[1,1,1]| and
A9: Dir111 = Dir u111 ;

per cases ( Dir100 = Dir010 or Dir100 = Dir001 or Dir100 = Dir111 or Dir010 = Dir001 or Dir010 = Dir111 or Dir001 = Dir111 ) by A1;

suppose A10: Dir100 = Dir010 ; :: thesis: contradiction

( not u100 is zero & not u010 is zero ) by A2, A4, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u100,u010 by A3, A5, A10, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A12: u100 = a * u010 by ANPROJ_1:1;
|[1,0,0]| = |[(a * 0),(a * 1),0]| by A2, A4, A12, EUCLID_5:8
.= |[0,a,0]| ;
then 1 = |[0,a,0]| `1 by EUCLID_5:2;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

suppose A13: Dir100 = Dir001 ; :: thesis: contradiction

( not u100 is zero & not u001 is zero ) by A2, A6, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u100,u001 by A13, A3, A7, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A15: u100 = a * u001 by ANPROJ_1:1;
|[1,0,0]| = |[(a * 0),(a * 0),(a * 1)]| by A2, A6, A15, EUCLID_5:8
.= |[0,0,a]| ;
then 1 = |[0,0,a]| `1 by EUCLID_5:2;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

suppose A16: Dir100 = Dir111 ; :: thesis: contradiction

( not u100 is zero & not u111 is zero ) by A2, A8, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u100,u111 by A16, A3, A9, ANPROJ_1:22;
then consider a being Real such that
A17: a <> 0 and
A18: u100 = a * u111 by ANPROJ_1:1;
|[1,0,0]| = |[(a * 1),(a * 1),(a * 1)]| by A2, A8, A18, EUCLID_5:8
.= |[a,a,a]| ;
then 0 = |[a,a,a]| `2 by EUCLID_5:2;
hence contradiction by A17, EUCLID_5:2; :: thesis: verum

end;

suppose A19: Dir010 = Dir001 ; :: thesis: contradiction

( not u010 is zero & not u001 is zero ) by A4, A6, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u010,u001 by A5, A7, A19, ANPROJ_1:22;
then consider a being Real such that
A20: a <> 0 and
A21: u010 = a * u001 by ANPROJ_1:1;
|[0,1,0]| = |[(a * 0),(a * 0),(a * 1)]| by A4, A6, A21, EUCLID_5:8
.= |[0,0,a]| ;
then 0 = |[0,0,a]| `3 by EUCLID_5:2;
hence contradiction by A20, EUCLID_5:2; :: thesis: verum

end;

suppose A22: Dir010 = Dir111 ; :: thesis: contradiction

( not u010 is zero & not u111 is zero ) by A4, A8, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u010,u111 by A22, A5, A9, ANPROJ_1:22;
then consider a being Real such that
A23: a <> 0 and
A24: u010 = a * u111 by ANPROJ_1:1;
|[0,1,0]| = |[(a * 1),(a * 1),a]| by A4, A8, A24, EUCLID_5:8
.= |[a,a,a]| ;
then 0 = |[a,a,a]| `1 by EUCLID_5:2;
hence contradiction by A23, EUCLID_5:2; :: thesis: verum

end;

suppose A25: Dir001 = Dir111 ; :: thesis: contradiction

( not u001 is zero & not u111 is zero ) by A6, A8, EUCLID_5:4, FINSEQ_1:78;
then are_Prop u001,u111 by A7, A9, A25, ANPROJ_1:22;
then consider a being Real such that
A26: a <> 0 and
A27: u001 = a * u111 by ANPROJ_1:1;
|[0,0,1]| = |[(a * 1),(a * 1),a]| by A6, A8, A27, EUCLID_5:8
.= |[a,a,a]| ;
then 0 = |[a,a,a]| `1 by EUCLID_5:2;
hence contradiction by A26, EUCLID_5:2; :: thesis: verum

end;

end;