let V be RealLinearSpace; :: thesis: for w, y, u, v, u1, v1, u2, v2 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 w, y, u, v, u1, v1, u2, v2 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 & u,v '||' u,v1 & u,v '||' u,u2 & 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 (Lambda (OASpace V)) 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 & p,q // p,q1 & p,q // p,p2 & p,q // p,q2 ) by A1, A3, Th3;
then ( LIN p,q,p1 & LIN p,q,q1 & LIN p,q,p2 & LIN p,q,q2 ) by AFF_1:def 1;
then ( LIN p1,q1,p2 & LIN p1,q1,q2 ) by A2, AFF_1:17;
then p1,q1 // p2,q2 by AFF_1:19;
hence u1,v1 '||' u2,v2 by A1, Th3; :: thesis: verum