let p, q, r be Point of (TOP-REAL 3); :: thesis: ( p <X> q = 0. (TOP-REAL 3) & r = |[1,1,1]| implies p,q,r are_LinDep )
assume that
A1: p <X> q = 0. (TOP-REAL 3) and
A2: r = |[1,1,1]| ; :: thesis: p,q,r are_LinDep
|[(((p `2) * (q `3)) - ((p `3) * (q `2))),(((p `3) * (q `1)) - ((p `1) * (q `3))),(((p `1) * (q `2)) - ((p `2) * (q `1)))]| = |[0,0,0]| by A1, EUCLID_5:def 4, EUCLID_5:4;
then ( ((p `2) * (q `3)) - ((p `3) * (q `2)) = |[0,0,0]| `1 & ((p `3) * (q `1)) - ((p `1) * (q `3)) = |[0,0,0]| `2 & ((p `1) * (q `2)) - ((p `2) * (q `1)) = |[0,0,0]| `3 ) by EUCLID_5:14;
then A3: ( ((p `2) * (q `3)) - ((p `3) * (q `2)) = 0 & ((p `3) * (q `1)) - ((p `1) * (q `3)) = 0 & ((p `1) * (q `2)) - ((p `2) * (q `1)) = 0 ) by EUCLID_5:14;
reconsider r = |[1,1,1]| as Element of (TOP-REAL 3) ;
|{p,q,r}| = 0

proof

( r `1 = 1 & r `2 = 1 & r `3 = 1 ) by EUCLID_5:2;
then |{p,q,r}| = (((((((p `1) * (q `2)) * 1) - (((p `3) * (q `2)) * 1)) - (((p `1) * (q `3)) * 1)) + (((p `2) * (q `3)) * 1)) - (((p `2) * (q `1)) * 1)) + (((p `3) * (q `1)) * 1) by Th23
.= 0 by A3 ;
hence |{p,q,r}| = 0 ; :: thesis: verum

end;

hence p,q,r are_LinDep by A2, Th37; :: thesis: verum