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

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