let SK be SubdivisionStr of K; :: thesis: SK is bounded
consider r being Real such that
A1: for A being Subset of (Euclid n) st A in the topology of K holds
( A is bounded & diameter A <= r ) by Def2;
take r ; :: according to SIMPLEX2:def 2,SIMPLEX2:def 5 :: thesis: for A being Subset of (Euclid n) st A in the topology of SK holds
( A is bounded & diameter A <= r )
let A be Subset of (Euclid n); :: thesis: ( A in the topology of SK implies ( A is bounded & diameter A <= r ) )
assume A2: A in the topology of SK ; :: thesis: ( A is bounded & diameter A <= r )
then reconsider a = A as Subset of SK ;
a is simplex-like by A2, PRE_TOPC:def 2;
then consider b being Subset of K such that
A3: b is simplex-like and
A4: conv (@ a) c= conv (@ b) by SIMPLEX1:def 4;
A5: [#] (TOP-REAL n) = [#] (Euclid n) by Lm1;
then reconsider cA = conv (@ a) as Subset of (Euclid n) ;
[#] K c= [#] (TOP-REAL n) by SIMPLEX0:def 9;
then reconsider B = b as Subset of (Euclid n) by A5, XBOOLE_1:1;
A6: B in the topology of K by A3, PRE_TOPC:def 2;
then A7: diameter B <= r by A1;
A8: B is bounded by A1, A6;
then @ b is bounded by JORDAN2C:11;
then conv (@ b) is bounded by Th14;
then reconsider cB = conv (@ b) as bounded Subset of (Euclid n) by JORDAN2C:11;
A9: diameter cA <= diameter cB by A4, TBSP_1:24;
cA c= cB by A4;
then A10: cA is bounded by TBSP_1:14;
then A is bounded by CONVEX1:41, TBSP_1:14;
then A11: diameter cA = diameter A by A10, Th15;
diameter cB = diameter B by A8, Th15;
hence ( A is bounded & diameter A <= r ) by A9, A10, A11, A7, CONVEX1:41, TBSP_1:14, XXREAL_0:2; :: thesis: verum