let V be RealLinearSpace; :: thesis: for K being with_empty_element SimplicialComplex of V st |.K.| c= [#] K holds
for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ) holds
subdivision (B,K) is SubdivisionStr of K

let K be with_empty_element SimplicialComplex of V; :: thesis: ( |.K.| c= [#] K implies for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ) holds
subdivision (B,K) is SubdivisionStr of K )

assume A1: |.K.| c= [#] K ; :: thesis: for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ) holds
subdivision (B,K) is SubdivisionStr of K

let B be Function of (BOOL the carrier of V), the carrier of V; :: thesis: ( ( for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ) implies subdivision (B,K) is SubdivisionStr of K )

assume A2: for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ; :: thesis: subdivision (B,K) is SubdivisionStr of K
set P = subdivision (B,K);
defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; :: thesis: S1[n + 1]
let x be set ; :: thesis: for A being Simplex of K st x in conv (@ A) & card A = n + 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 )

let A be Simplex of K; :: thesis: ( x in conv (@ A) & card A = n + 1 implies 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 ) )

assume that
A6: x in conv (@ A) and
A7: card A = n + 1 ; :: thesis: 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 )

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 ;
A13: B .: {A} = Im (B,A) by RELAT_1:def 16;
then A14: B .: {A} = {BA} by ;
( BA in conv A1 & conv A1 c= |.K.| ) by ;
then BA in |.K.| ;
then ( [#] (subdivision (B,K)) = [#] K & {BA} is Subset of K ) by ;
then reconsider BY = B .: {A} as Subset of (subdivision (B,K)) by ;
per cases ( x = B . A or x <> B . A ) ;
suppose A15: x = B . A ; :: thesis: 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 )

now :: thesis: for x1, x2 being set st x1 in {A} & x2 in {A} holds
x1,x2 are_c=-comparable
let x1, x2 be set ; :: thesis: ( x1 in {A} & x2 in {A} implies x1,x2 are_c=-comparable )
assume that
A16: x1 in {A} and
A17: x2 in {A} ; :: thesis: x1,x2 are_c=-comparable
x1 = A by ;
hence x1,x2 are_c=-comparable by ; :: thesis: verum
end;
then reconsider Y = {A} as c=-linear finite simplex-like Subset-Family of K by ;
take Y ; :: thesis: ex BS being Subset of (subdivision (B,K)) st
( BS = B .: Y & x in conv (@ BS) & union Y c= A )

take BY ; :: thesis: ( BY = B .: Y & x in conv (@ BY) & union Y c= A )
conv {BA} = {BA} by RLAFFIN1:1;
hence ( BY = B .: Y & x in conv (@ BY) & union Y c= A ) by ; :: thesis: verum
end;
suppose x <> B . A ; :: thesis: 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 )

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 ;
( @ (A \ {p}) = A1 \ {p} & card (A \ {p}) = n ) by ;
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 ;
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: ( x1 in S \/ {A} & x2 in S \/ {A} implies x1,x2 are_c=-comparable )
assume A26: ( x1 in S \/ {A} & x2 in S \/ {A} ) ; :: thesis: x1,x2 are_c=-comparable
end;
then reconsider S1 = S \/ {A} as c=-linear finite simplex-like Subset-Family of K by ;
A28: B .: S1 = BS \/ BY by ;
then reconsider BS1 = B .: S1 as Subset of (subdivision (B,K)) ;
A29: conv (@ BS) c= conv (@ BS1) by ;
BA in BY by ;
then A30: BA in @ BS1 by ;
take S1 ; :: thesis: ex BS being Subset of (subdivision (B,K)) st
( BS = B .: S1 & x in conv (@ BS) & union S1 c= A )

take BS1 ; :: thesis: ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A )
A31: @ BS1 c= conv (@ BS1) by CONVEX1:41;
union S1 = () \/ A by
.= A by ;
hence ( BS1 = B .: S1 & x in conv (@ BS1) & union S1 c= A ) by ; :: thesis: verum
end;
end;
end;
A32: S1[ 0 ]
proof
let x be set ; :: thesis: for A being Simplex of K st x in conv (@ A) & card A = 0 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 )

let A be Simplex of K; :: thesis: ( x in conv (@ A) & card A = 0 implies 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 ) )

assume that
A33: x in conv (@ A) and
A34: card A = 0 ; :: thesis: 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 )

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: verum
end;
A35: for n being Nat holds S1[n] from NAT_1:sch 2(A32, A4);
thus |.K.| c= |.(subdivision (B,K)).| :: according to SIMPLEX1:def 4 :: thesis: 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 x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.K.| or x in |.(subdivision (B,K)).| )
assume x in |.K.| ; :: thesis: x in |.(subdivision (B,K)).|
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;
S1[ 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 ;
then conv (@ BS) c= |.(subdivision (B,K)).| by Th5;
hence x in |.(subdivision (B,K)).| by A39; :: thesis: verum
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: ( A is simplex-like implies ex B being Subset of K st
( B is simplex-like & conv (@ A) c= conv (@ B) ) )

assume A is simplex-like ; :: thesis: ex B being Subset of K st
( B is simplex-like & conv (@ A) c= conv (@ B) )

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 ( S is empty or not S is empty ) ;
suppose A41: S is empty ; :: thesis: ex B being Subset of K st
( B is simplex-like & conv (@ A) c= conv (@ B) )

take {} K ; :: thesis: ( {} K is simplex-like & conv (@ A) c= conv (@ ({} K)) )
thus ( {} K is simplex-like & conv (@ A) c= conv (@ ({} K)) ) by ; :: thesis: verum
end;
suppose A42: not S is empty ; :: thesis: ex B being Subset of K st
( B is simplex-like & conv (@ A) c= conv (@ B) )

take U = union S; :: thesis: ( U is simplex-like & conv (@ A) c= conv (@ U) )
A43: A c= conv (@ U)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in conv (@ U) )
assume x in A ; :: thesis: x in conv (@ U)
then consider y being object such that
A44: y in dom B and
A45: y in S and
A46: B . y = x by ;
reconsider y = y as Simplex of K by ;
y <> {} by ;
then A47: B . y in conv (@ y) by A2;
conv (@ y) c= conv (@ U) by ;
hence x in conv (@ U) by ; :: thesis: verum
end;
U in S by ;
hence ( U is simplex-like & conv (@ A) c= conv (@ U) ) by ; :: thesis: verum
end;
end;
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: verum