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