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

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