:: deftheorem defines satisfying_Gen_Par_Pasch PASCH:def 3 :
for OAS being OAffinSpace holds
( OAS is satisfying_Gen_Par_Pasch iff for a, b, c, a9, b9, c9 being Element of OAS st not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear holds
Mid a9,b9,c9 );