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

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