let SK be SubdivisionStr of K; 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
; SIMPLEX2:def 2,SIMPLEX2:def 5 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); ( A in the topology of SK implies ( A is bounded & diameter A <= r ) )
assume A2:
A in the topology of SK
; ( 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; verum