let V be RealLinearSpace; :: thesis: for w, y, u, v, u1, v1, u2, v2 being VECTOR of 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 w, y, u, v, u1, v1, u2, v2 be VECTOR of ; :: 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 p' = u, q' = v, p1' = u1, q1' = v1, p2' = u2, q2' = v2 as Element of by ANALMETR:22;
reconsider S' = OASpace V as OAffinSpace by A1, Th1;
reconsider S = Lambda S' as AffinSpace by DIRAF:48;
reconsider p = p', q = q', p1 = p1', q1 = q1', p2 = p2', q2 = q2' 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:17;
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:17;
then p1,q1 // p2,q2 by A9, AFF_1:19;
hence u1,v1 '||' u2,v2 by A1, Th3; :: thesis: verum