consider S being object such that
A1: S in the topology of K by XBOOLE_0:def 1;
reconsider S = S as Simplex of K by A1, PRE_TOPC:def 2;
S is finite ;
hence ex b₁ being Simplex of K st b₁ is finite ; :: thesis: verum