let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= B & B is Affine holds
Affin A c= B
let A, B be Subset of RLS; :: thesis: ( A c= B & B is Affine implies Affin A c= B )
assume ( A c= B & B is Affine ) ; :: thesis: Affin A c= B
then B in { C where C is Affine Subset of RLS : A c= C } ;
hence Affin A c= B by SETFAM_1:3; :: thesis: verum