let V be RealLinearSpace; :: thesis: for u, u1, v, v1 being VECTOR of V
for p, p1, q, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, u1, v, v1 be VECTOR of V; :: thesis: for p, p1, q, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let p, p1, q, q1 be Element of (Lambda (OASpace V)); :: thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) )
assume A1: ( p = u & q = v & p1 = u1 & q1 = v1 ) ; :: thesis: ( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )

hereby :: thesis: ( ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) implies p,q // p1,q1 )

assume p,q // p1,q1 ; :: thesis: ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) )
then [[p,q],[p1,q1]] in the CONGR of (Lambda (OASpace V)) by ANALOAF:def 2;
then [[u,v],[u1,v1]] in lambda (DirPar V) by A1, Th17;
hence ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by Th15; :: thesis: verum

end;

given a, b being Real such that A2: ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ; :: thesis: p,q // p1,q1
[[u,v],[u1,v1]] in lambda (DirPar V) by A2, Th15;
then [[p,q],[p1,q1]] in the CONGR of (Lambda (OASpace V)) by A1, Th17;
hence p,q // p1,q1 by ANALOAF:def 2; :: thesis: verum