let AFS be AffinSpace; :: thesis: id the carrier of AFS is translation
id the carrier of AFS is dilatation by Th86;
hence id the carrier of AFS is translation by Def11; :: thesis: verum