let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y 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 u, u1, v, v1, w, y 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 :: thesis: ( p,q // p1,q1 implies u,v '||' u1,v1 )

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:22;
then ( u,v // u1,v1 or u,v // v1,u1 ) by ANALMETR:14;
hence u,v '||' u1,v1 ; :: thesis: verum

end;

now :: thesis: ( u,v '||' u1,v1 implies p,q // p1,q1 )

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

end;

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