let OAS be OAffinSpace; :: thesis: id the carrier of OAS is positive_dilatation
OAS is CongrSpace by Th26;
then id the carrier of OAS is_DIL_of OAS by Th23;
hence id the carrier of OAS is positive_dilatation ; :: thesis: verum