let V be RealLinearSpace; :: thesis: for u, u1, u2, v, v1, v2, w, y being VECTOR of V st Gen w,y & u <> v & u,v '||' u,u1 & u,v '||' u,v1 & u,v '||' u,u2 & u,v '||' u,v2 holds
u1,v1 '||' u2,v2
let u, u1, u2, v, v1, v2, w, y be VECTOR of V; :: thesis: ( Gen w,y & u <> v & u,v '||' u,u1 & u,v '||' u,v1 & u,v '||' u,u2 & u,v '||' u,v2 implies u1,v1 '||' u2,v2 )
assume that
A1: Gen w,y and
A2: u <> v and
A3: u,v '||' u,u1 and
A4: u,v '||' u,v1 and
A5: u,v '||' u,u2 and
A6: u,v '||' u,v2 ; :: thesis: u1,v1 '||' u2,v2
reconsider p9 = u, q9 = v, p19 = u1, q19 = v1, p29 = u2, q29 = v2 as Element of (Lambda (OASpace V)) by ANALMETR:16;
reconsider S9 = OASpace V as OAffinSpace by A1, Th1;
reconsider S = Lambda S9 as AffinSpace by DIRAF:41;
reconsider p = p9, q = q9, p1 = p19, q1 = q19, p2 = p29, q2 = q29 as Element of the carrier of S ;
p,q // p,p1 by A1, A3, Th3;
then A7: LIN p,q,p1 by AFF_1:def 1;
p,q // p,q1 by A1, A4, Th3;
then A8: LIN p,q,q1 by AFF_1:def 1;
p,q // p,q2 by A1, A6, Th3;
then LIN p,q,q2 by AFF_1:def 1;
then A9: LIN p1,q1,q2 by A2, A7, A8, AFF_1:8;
p,q // p,p2 by A1, A5, Th3;
then LIN p,q,p2 by AFF_1:def 1;
then LIN p1,q1,p2 by A2, A7, A8, AFF_1:8;
then p1,q1 // p2,q2 by A9, AFF_1:10;
hence u1,v1 '||' u2,v2 by A1, Th3; :: thesis: verum