let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= Affin B holds
Affin (A \/ B) = Affin B
let A, B be Subset of RLS; :: thesis: ( A c= Affin B implies Affin (A \/ B) = Affin B )
assume A1: A c= Affin B ; :: thesis: Affin (A \/ B) = Affin B
set AB = { C where C is Affine Subset of RLS : A \/ B c= C } ;
B c= Affin B by Lm7;
then A \/ B c= Affin B by A1, XBOOLE_1:8;
then Affin B in { C where C is Affine Subset of RLS : A \/ B c= C } ;
then A2: Affin (A \/ B) c= Affin B by SETFAM_1:3;
Affin B c= Affin (A \/ B) by Th52, XBOOLE_1:7;
hence Affin (A \/ B) = Affin B by A2; :: thesis: verum