let OAS be OAffinSpace; :: thesis: Lambda OAS is CongrSpace
Lambda OAS is AffinSpace by DIRAF:41;
hence Lambda OAS is CongrSpace by Th82; :: thesis: verum