let V be RealLinearSpace; :: thesis: for w, y, u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of the carrier of (AMSpace V,w,y) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 )
let w, y, u, v, u1, v1 be VECTOR of V; :: thesis: for p, q, p1, q1 being Element of the carrier of (AMSpace V,w,y) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 )
let p, q, p1, q1 be Element of the carrier of (AMSpace V,w,y); :: thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff u,v '||' u1,v1 ) )
assume A1: ( p = u & q = v & p1 = u1 & q1 = v1 ) ; :: thesis: ( p,q // p1,q1 iff u,v '||' u1,v1 )

A2: now

assume u,v '||' u1,v1 ; :: thesis: p,q // p1,q1
then ( u,v // u1,v1 or u,v // v1,u1 ) by Def1;
then ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by ANALMETR:18;
hence p,q // p1,q1 by A1, ANALMETR:32; :: thesis: verum

end;

now

assume p,q // p1,q1 ; :: thesis: u,v '||' u1,v1
then ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A1, ANALMETR:32;
then ( u,v // u1,v1 or u,v // v1,u1 ) by ANALMETR:18;
hence u,v '||' u1,v1 by Def1; :: thesis: verum

end;

hence ( p,q // p1,q1 iff u,v '||' u1,v1 ) by A2; :: thesis: verum