let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= B holds
Affin A c= Affin B
let A, B be Subset of RLS; :: thesis: ( A c= B implies Affin A c= Affin B )
assume A1: A c= B ; :: thesis: Affin A c= Affin B
B c= Affin B by Lm7;
then A c= Affin B by A1;
hence Affin A c= Affin B by Th51; :: thesis: verum