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

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