assume A1:
( Dir100 = Dir010 or Dir100 = Dir001 or Dir100 = Dir111 or Dir010 = Dir001 or Dir010 = Dir111 or Dir001 = Dir111 )
; 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
;
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;
verum end; suppose A13:
Dir100 = Dir001
;
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;
verum end; suppose A16:
Dir100 = Dir111
;
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;
verum end; suppose A19:
Dir010 = Dir001
;
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;
verum end; suppose A22:
Dir010 = Dir111
;
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;
verum end; suppose A25:
Dir001 = Dir111
;
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;
verum end; end;