for OAS being OAffinSpace holds OAS is satisfying_Ext_Bet_Pasch by Th27;