let OAS be OAffinSpace; :: thesis: id the carrier of OAS is positive_dilatation
OAS is CongrSpace by Th40;
then id the carrier of OAS is_DIL_of OAS by Th37;
hence id the carrier of OAS is positive_dilatation by Def6; :: thesis: verum