let V be non empty RLSStruct ; :: thesis: for A being Subset of V holds A c= Affin A
let A be Subset of V; :: thesis: A c= Affin A
set BB = { B where B is Affine Subset of V : A c= B } ;

A1: now :: thesis: for Y being set st Y in { B where B is Affine Subset of V : A c= B } holds
A c= Y

let Y be set ; :: thesis: ( Y in { B where B is Affine Subset of V : A c= B } implies A c= Y )
assume Y in { B where B is Affine Subset of V : A c= B } ; :: thesis: A c= Y
then ex B being Affine Subset of V st
( Y = B & A c= B ) ;
hence A c= Y ; :: thesis: verum

end;

[#] V is Affine ;
then [#] V in { B where B is Affine Subset of V : A c= B } ;
hence A c= Affin A by A1, SETFAM_1:5; :: thesis: verum