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 ;

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;

end;

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;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

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;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

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;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

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;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

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;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

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;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