let a, b, c, d be Real; for u, v being non zero Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,0]| holds
Dir u <> Dir v
let u, v be non zero Element of (TOP-REAL 3); ( u = |[a,b,1]| & v = |[c,d,0]| implies Dir u <> Dir v )
assume that
A1:
u = |[a,b,1]|
and
A2:
v = |[c,d,0]|
; Dir u <> Dir v
assume
Dir u = Dir v
; contradiction
then
are_Prop u,v
by ANPROJ_1:22;
then consider x being Real such that
x <> 0
and
A3:
u = x * v
by ANPROJ_1:1;
1 =
(x * v) `3
by A3, A1, EUCLID_5:2
.=
|[(x * (v `1)),(x * (v `2)),(x * (v `3))]| `3
by EUCLID_5:7
.=
x * (v `3)
by EUCLID_5:2
.=
x * 0
by A2, EUCLID_5:2
.=
0
;
hence
contradiction
; verum