theorem Th3: :: GEOMTRAP:3

for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V st Gen w,y holds
for p, q, p1, q1 being Element of the carrier of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff u,v '||' u1,v1 )