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

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