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

Lambda OAS is AffinSpace by DIRAF:41;

hence Lambda OAS is CongrSpace by Th66; :: thesis: verum