set T = TOP-REAL n;
take C = Complex_of {({} (TOP-REAL n))}; :: thesis: ( C is bounded & C is affinely-independent & C is simplex-join-closed & not C is void & C is finite-degree & C is total )
C is Euclid n bounded by Th6;
hence ( C is bounded & C is affinely-independent & C is simplex-join-closed & not C is void & C is finite-degree & C is total ) ; :: thesis: verum