let a, b, c, d be Real; :: thesis: 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); :: thesis: ( 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]| ; :: thesis: Dir u <> Dir v

assume Dir u = Dir v ; :: thesis: 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 ; :: thesis: verum

Dir u <> Dir v

let u, v be non zero Element of (TOP-REAL 3); :: thesis: ( 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]| ; :: thesis: Dir u <> Dir v

assume Dir u = Dir v ; :: thesis: 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 ; :: thesis: verum