theorem :: PASCH:22

for OAS being OAffinSpace
for a, b, c being Element of OAS ex x being Element of OAS st
( a,x // b,c & a,b // x,c )