for OAS being OAffinSpace st OAS is satisfying_DES_1 holds
OAS is satisfying_DES