for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
( OAS is satisfying_DES_1 & OAS is satisfying_DES ) by Th6, Th11;