set TRn = TOP-REAL n;
consider I being affinely-independent Subset of (TOP-REAL n) such that
A1: Affn c= I and
I c= [#] (TOP-REAL n) and
A2: Affin I = Affin ([#] (TOP-REAL n)) by RLAFFIN1:60;
A3: dim (TOP-REAL n) = n by Th4;
[#] (TOP-REAL n) is Affine by RUSUB_4:22;
then Affin I = [#] (TOP-REAL n) by A2, RLAFFIN1:50;
then card I = n + 1 by A3, Th6;
then conv I is closed by Lm9;
then (conv I) /\ (Affin Affn) is closed ;
hence conv Affn is closed by A1, Th9; :: thesis: verum