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 } ;

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

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

[#] V is Affine
;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;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

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