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