theorem :: PASCH:28

for OAS being OAffinSpace holds OAS is satisfying_Ext_Bet_Pasch by Th27;