let V be RealLinearSpace; :: thesis:
let K be with_empty_element SimplicialComplex of V; :: thesis:
assume A1: |.K.| c= [#] K ; :: thesis:
let B be Function of (BOOL the carrier of V), the carrier of V; :: thesis:
assume A2: for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ; :: thesis:
set P = subdivision (B,K);
defpred S₁[ Nat] means for x being set
for A being Simplex of K st x in conv (@ A) & card A = $1 holds
ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st
( BS = B .: S & x in conv (@ BS) & union S c= A );
A3: dom B = BOOL the carrier of V by FUNCT_2:def 1;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A5: S₁[n] ; :: thesis:
let x be set ; :: thesis:
let A be Simplex of K; :: thesis:
assume that
A6: x in conv (@ A) and
A7: card A = n + 1 ; :: thesis:
reconsider A1 = @ A as non empty Subset of V by A6;
A8: union {A} = A by ZFMISC_1:25;
A9: for P being Subset of K st P in {A} holds
P is simplex-like by TARSKI:def 1;
then A10: {A} is simplex-like ;
A11: B . A1 in conv (@ A) by A2;
then reconsider BA = B . A as Element of V ;
A1 = A ;
then A12: A in dom B by A3, ZFMISC_1:56;
A13: B .: {A} = Im (B,A) by RELAT_1:def 16;
then A14: B .: {A} = {BA} by A12, FUNCT_1:59;
( BA in conv A1 & conv A1 c= |.K.| ) by A2, Th5;
then BA in |.K.| ;
then ( [#] (subdivision (B,K)) = [#] K & {BA} is Subset of K ) by A1, SIMPLEX0:def 20, ZFMISC_1:31;
then reconsider BY = B .: {A} as Subset of (subdivision (B,K)) by A12, A13, FUNCT_1:59;

per cases ;

suppose A15: x = B . A ; :: thesis:

now :: thesis:

let x1, x2 be set ; :: thesis:
assume that
A16: x1 in {A} and
A17: x2 in {A} ; :: thesis:
x1 = A by A16, TARSKI:def 1;
hence x1,x2 are_c=-comparable by A17, TARSKI:def 1; :: thesis:

end;

then reconsider Y = {A} as c=-linear finite simplex-like Subset-Family of K by A9, ORDINAL1:def 8, TOPS_2:def 1;
take Y ; :: thesis:
take BY ; :: thesis:
conv {BA} = {BA} by RLAFFIN1:1;
hence ( BY = B .: Y & x in conv (@ BY) & union Y c= A ) by A14, A15, TARSKI:def 1, ZFMISC_1:25; :: thesis:

end;

suppose x <> B . A ; :: thesis:

then consider p, w being Element of V, r being Real such that
A18: p in A and
A19: w in conv (A1 \ {p}) and
A20: ( 0 <= r & r < 1 & (r * BA) + ((1 - r) * w) = x ) by A6, A11, RLAFFIN2:26;
( @ (A \ {p}) = A1 \ {p} & card (A \ {p}) = n ) by A7, A18, STIRL2_1:55;
then consider S being c=-linear finite simplex-like Subset-Family of K, BS being Subset of (subdivision (B,K)) such that
A21: BS = B .: S and
A22: w in conv (@ BS) and
A23: union S c= A \ {p} by A5, A19;
set S1 = S \/ {A};
A24: A \ {p} c= A by XBOOLE_1:36;
then A25: union S c= A by A23;
for x1, x2 being set st x1 in S \/ {A} & x2 in S \/ {A} holds
x1,x2 are_c=-comparable

proof

let x1, x2 be set ; :: thesis:
assume A26: ( x1 in S \/ {A} & x2 in S \/ {A} ) ; :: thesis:

per cases by A26, XBOOLE_0:def 3;

suppose ( x1 in S & x2 in S ) ; :: thesis:

hence x1,x2 are_c=-comparable by ORDINAL1:def 8; :: thesis:

end;

suppose ( x1 in S & x2 in {A} ) ; :: thesis:

then ( x1 c= union S & x2 = A ) by TARSKI:def 1, ZFMISC_1:74;
then x1 c= x2 by A25;
hence x1,x2 are_c=-comparable ; :: thesis:

end;

suppose ( x2 in S & x1 in {A} ) ; :: thesis:

then ( x2 c= union S & x1 = A ) by TARSKI:def 1, ZFMISC_1:74;
then x2 c= x1 by A25;
hence x1,x2 are_c=-comparable ; :: thesis:

end;

suppose A27: ( x1 in {A} & x2 in {A} ) ; :: thesis:

then x1 = A by TARSKI:def 1;
hence x1,x2 are_c=-comparable by A27, TARSKI:def 1; :: thesis:

end;

then reconsider S1 = S \/ {A} as c=-linear finite simplex-like Subset-Family of K by A10, ORDINAL1:def 8, TOPS_2:13;
A28: B .: S1 = BS \/ BY by A21, RELAT_1:120;
then reconsider BS1 = B .: S1 as Subset of (subdivision (B,K)) ;
A29: conv (@ BS) c= conv (@ BS1) by A28, RLTOPSP1:20, XBOOLE_1:7;
BA in BY by A14, TARSKI:def 1;
then A30: BA in @ BS1 by A28, XBOOLE_0:def 3;
take S1 ; :: thesis:
take BS1 ; :: thesis:
A31: @ BS1 c= conv (@ BS1) by CONVEX1:41;
union S1 = (union S) \/ A by A8, ZFMISC_1:78
.= A by A23, A24, XBOOLE_1:1, XBOOLE_1:12 ;
hence ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A ) by A20, A22, A29, A30, A31, RLTOPSP1:def 1; :: thesis:

end;

A32: S₁[ 0 ]

proof

let x be set ; :: thesis:
let A be Simplex of K; :: thesis:
assume that
A33: x in conv (@ A) and
A34: card A = 0 ; :: thesis:
not @ A is empty by A33;
hence ex S being c=-linear finite simplex-like Subset-Family of K ex BS being Subset of (subdivision (B,K)) st
( BS = B .: S & x in conv (@ BS) & union S c= A ) by A34; :: thesis:

end;

A35: for n being Nat holds S₁[n] from NAT_1:sch 2(A32, A4);
thus |.K.| c= |.(subdivision (B,K)).| :: according to SIMPLEX1:def 4 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in |.K.| ; :: thesis:
then consider A being Subset of K such that
A36: A is simplex-like and
A37: x in conv (@ A) by Def3;
reconsider A = A as Simplex of K by A36;
S₁[ card A] by A35;
then consider S being c=-linear finite simplex-like Subset-Family of K, BS being Subset of (subdivision (B,K)) such that
A38: BS = B .: S and
A39: x in conv (@ BS) and
union S c= A by A37;
BS is simplex-like by A38, SIMPLEX0:def 20;
then conv (@ BS) c= |.(subdivision (B,K)).| by Th5;
hence x in |.(subdivision (B,K)).| by A39; :: thesis:

end;

for A being Subset of (subdivision (B,K)) st A is simplex-like holds
ex B being Subset of K st
( B is simplex-like & conv (@ A) c= conv (@ B) )

proof

let A be Subset of (subdivision (B,K)); :: thesis:
assume A is simplex-like ; :: thesis:
then consider S being c=-linear finite simplex-like Subset-Family of K such that
A40: A = B .: S by SIMPLEX0:def 20;

per cases ;

suppose A41: S is empty ; :: thesis:

take {} K ; :: thesis:
thus ( {} K is simplex-like & conv (@ A) c= conv (@ ({} K)) ) by A40, A41; :: thesis:

end;

suppose A42: not S is empty ; :: thesis:

take U = union S; :: thesis:
A43: A c= conv (@ U)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then consider y being object such that
A44: y in dom B and
A45: y in S and
A46: B . y = x by A40, FUNCT_1:def 6;
reconsider y = y as Simplex of K by A45, TOPS_2:def 1;
y <> {} by A44, ZFMISC_1:56;
then A47: B . y in conv (@ y) by A2;
conv (@ y) c= conv (@ U) by A45, RLTOPSP1:20, ZFMISC_1:74;
hence x in conv (@ U) by A46, A47; :: thesis:

end;

U in S by A42, SIMPLEX0:9;
hence ( U is simplex-like & conv (@ A) c= conv (@ U) ) by A43, CONVEX1:30, TOPS_2:def 1; :: thesis:

end;

hence for A being Subset of (subdivision (B,K)) st A is simplex-like holds
ex B being Subset of K st
( B is simplex-like & conv (@ A) c= conv (@ B) ) ; :: thesis: