let V be RealLinearSpace; :: thesis: for A, B being Subset of V st conv A c= conv B holds

Affin A c= Affin B

let A, B be Subset of V; :: thesis: ( conv A c= conv B implies Affin A c= Affin B )

( Affin (conv A) = Affin A & Affin (conv B) = Affin B ) by Th67;

hence ( conv A c= conv B implies Affin A c= Affin B ) by Th52; :: thesis: verum

Affin A c= Affin B

let A, B be Subset of V; :: thesis: ( conv A c= conv B implies Affin A c= Affin B )

( Affin (conv A) = Affin A & Affin (conv B) = Affin B ) by Th67;

hence ( conv A c= conv B implies Affin A c= Affin B ) by Th52; :: thesis: verum