let V be non empty RLSStruct ; :: thesis: for A being Affine Subset of V holds A = Affin A
let A be Affine Subset of V; :: thesis: A = Affin A
set BB = { B where B is Affine Subset of V : A c= B } ;
A in { B where B is Affine Subset of V : A c= B } ;
then A1: Affin A c= A by SETFAM_1:3;
A c= Affin A by Lm7;
hence A = Affin A by A1; :: thesis: verum