let V be RealLinearSpace; :: thesis: for u, v, u1, v1 being VECTOR of V holds
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, v, u1, v1 be VECTOR of V; :: thesis: ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ( [[u,v],[u1,v1]] in DirPar V or [[u,v],[v1,u1]] in DirPar V ) ) by DIRAF:def 1;
then ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ( u,v // u1,v1 or u,v // v1,u1 ) ) by ANALOAF:33;
hence ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) by Th18; :: thesis: verum