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