:: deftheorem defines satisfying_Ext_Par_Pasch PASCH:def 2 :
for OAS being OAffinSpace holds
( OAS is satisfying_Ext_Par_Pasch iff for a, b, c, d, p being Element of OAS st Mid p,b,c & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear holds
Mid p,a,d );