theorem Th8: :: PAPDESAF:8
for OAS being OAffinSpace
for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds
( o,b // o,b9 & a,b // a9,b9 )