let V be RealLinearSpace; :: thesis:
let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis:
set B = center_of_mass V;
set BC = BCS Kas;
defpred S₁[ Nat] means for S1, S2 being c=-linear finite simplex-like Subset-Family of Kas
for A1, A2 being Simplex of (BCS Kas) st A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= $1 & card (union S2) <= $1 & Int (@ A1) meets Int (@ A2) holds
A1 = A2;
assume A1: |.Kas.| c= [#] Kas ; :: thesis:
then A2: BCS Kas = subdivision ((center_of_mass V),Kas) by Def5;
A3: BCS Kas is affinely-independent by A1, Th28;
A4: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A6: S₁[n] ; :: thesis:
let S1, S2 be c=-linear finite simplex-like Subset-Family of Kas; :: thesis:
let A1, A2 be Simplex of (BCS Kas); :: thesis:
assume that
A7: A1 = (center_of_mass V) .: S1 and
A8: A2 = (center_of_mass V) .: S2 and
A9: card (union S1) <= n + 1 and
card (union S2) <= n + 1 and
A10: Int (@ A1) meets Int (@ A2) ; :: thesis:
A11: ( union S2 in S2 or S2 is empty ) by SIMPLEX0:9;
then A12: union S2 is simplex-like by TOPS_2:def 1, ZFMISC_1:2;
set U = union S1;
( S2 c= bool (union S2) & bool (@ (union S2)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;
then A13: S2 is Subset-Family of V by XBOOLE_1:1;
A14: ( union S1 in S1 or S1 is empty ) by SIMPLEX0:9;
then A15: union S1 is simplex-like by TOPS_2:def 1, ZFMISC_1:2;
( S1 c= bool (union S1) & bool (@ (union S1)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;
then A16: S1 is Subset-Family of V by XBOOLE_1:1;
then A17: Int ((center_of_mass V) .: S1) c= Int (@ (union S1)) by A15, RLAFFIN2:30;
Int (@ (union S1)) meets Int ((center_of_mass V) .: S2) by A7, A8, A10, A15, A16, RLAFFIN2:30, XBOOLE_1:63;
then Int (@ (union S1)) meets Int (@ (union S2)) by A13, A12, RLAFFIN2:30, XBOOLE_1:63;
then A18: union S1 = union S2 by A12, A15, Th25;

per cases by A9, NAT_1:8;

suppose card (union S1) <= n ; :: thesis:

hence A1 = A2 by A6, A7, A8, A10, A18; :: thesis:

end;

suppose A19: card (union S1) = n + 1 ; :: thesis:

then A20: not @ (union S1) is empty ;
then A21: union S1 in dom (center_of_mass V) by A4, ZFMISC_1:56;
then A22: (center_of_mass V) . (union S1) in @ A1 by A7, A14, A19, FUNCT_1:def 6, ZFMISC_1:2;
then reconsider Bu = (center_of_mass V) . (union S1) as Element of V ;
A23: {Bu} c= @ A1 by A22, ZFMISC_1:31;
A24: (center_of_mass V) . (union S1) in @ A2 by A8, A11, A18, A19, A21, FUNCT_1:def 6, ZFMISC_1:2;
then A25: {Bu} c= @ A2 by ZFMISC_1:31;
A26: Bu in {Bu} by ZFMISC_1:31;
A27: conv {Bu} = {Bu} by RLAFFIN1:1;
consider x being object such that
A28: x in Int (@ A1) and
A29: x in Int (@ A2) by A10, XBOOLE_0:3;
reconsider x = x as Element of V by A28;

per cases ;

suppose ( A1 = {Bu} & A2 = {Bu} ) ; :: thesis:

hence A1 = A2 ; :: thesis:

end;

suppose A30: ( A1 = {Bu} & A2 <> {Bu} ) ; :: thesis:

then ( {Bu} c< @ A2 & Int (@ A1) = @ A1 ) by A25, RLAFFIN2:6;
hence A1 = A2 by A27, A28, A29, A30, RLAFFIN2:def 1; :: thesis:

end;

suppose A31: ( A1 <> {Bu} & A2 = {Bu} ) ; :: thesis:

then ( {Bu} c< @ A1 & Int (@ A2) = @ A2 ) by A23, RLAFFIN2:6;
hence A1 = A2 by A27, A28, A29, A31, RLAFFIN2:def 1; :: thesis:

end;

suppose ( A1 <> {Bu} & A2 <> {Bu} ) ; :: thesis:

then {Bu} c< @ A1 by A23;
then A32: Bu <> x by A26, A27, A28, RLAFFIN2:def 1;
( S1 \ {(union S1)} c= S1 & S2 \ {(union S1)} c= S2 ) by XBOOLE_1:36;
then reconsider s1u = S1 \ {(union S1)}, s2u = S2 \ {(union S1)} as c=-linear finite simplex-like Subset-Family of Kas by TOPS_2:11;
A33: S1 c= the topology of Kas

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: x in S1 ; :: thesis:
then reconsider A = x as Subset of Kas ;
A is simplex-like by A34, TOPS_2:def 1;
hence x in the topology of Kas ; :: thesis:

end;

[#] Kas c= the carrier of V by SIMPLEX0:def 9;
then bool the carrier of Kas c= bool the carrier of V by ZFMISC_1:67;
then reconsider S1U = s1u, S2U = s2u as Subset-Family of V by XBOOLE_1:1;
set Bu1 = x |-- (@ A1);
set Bu2 = x |-- (@ A2);
set BT = (center_of_mass V) | the topology of Kas;
A35: S1 \ {(union S1)} c= S1 by XBOOLE_1:36;
A36: {(union S1)} c= S1 by A14, A19, ZFMISC_1:2, ZFMISC_1:31;
A37: union s2u c= union S1 by A18, XBOOLE_1:36, ZFMISC_1:77;
union s2u <> union S1

proof

assume A38: union s2u = union S1 ; :: thesis:
then union s2u in s2u by A20, SIMPLEX0:9, ZFMISC_1:2;
hence contradiction by A38, ZFMISC_1:56; :: thesis:

end;

then A39: union s2u c< union S1 by A37;
then consider xS2U being object such that
A40: xS2U in @ (union S1) and
A41: not xS2U in union S2U by XBOOLE_0:6;
reconsider xS2U = xS2U as Element of V by A40;
union S2U c= (union S1) \ {xS2U} by A37, A41, ZFMISC_1:34;
then A42: conv (union S2U) c= conv (@ ((union S1) \ {xS2U})) by RLAFFIN1:3;
A43: x in conv (@ A1) by A28, RLAFFIN2:def 1;
then A44: (x |-- (@ A1)) . Bu <= 1 by A3, RLAFFIN1:71;
A45: (x |-- (@ A1)) . Bu < 1

proof

assume (x |-- (@ A1)) . Bu >= 1 ; :: thesis:
then (x |-- (@ A1)) . Bu = 1 by A44, XXREAL_0:1;
hence contradiction by A3, A32, A43, RLAFFIN1:72; :: thesis:

end;

conv (@ A1) c= Affin (@ A1) by RLAFFIN1:65;
then A46: x = Sum (x |-- (@ A1)) by A3, A43, RLAFFIN1:def 7;
then Bu in Carrier (x |-- (@ A1)) by A3, A22, A28, A43, RLAFFIN1:71, RLAFFIN2:11;
then A47: (x |-- (@ A1)) . Bu <> 0 by RLVECT_2:19;
x |-- (@ A1) is convex by A3, A43, RLAFFIN1:71;
then consider p1 being Element of V such that
A48: p1 in conv ((@ A1) \ {Bu}) and
A49: x = (((x |-- (@ A1)) . Bu) * Bu) + ((1 - ((x |-- (@ A1)) . Bu)) * p1) and
((1 / ((x |-- (@ A1)) . Bu)) * x) + ((1 - (1 / ((x |-- (@ A1)) . Bu))) * p1) = Bu by A32, A46, A47, RLAFFIN2:1;
A50: p1 in Int ((@ A1) \ {Bu}) by A3, A22, A28, A48, A49, RLAFFIN2:14;
A51: {Bu} = Im ((center_of_mass V),(union S1)) by A21, FUNCT_1:59
.= (center_of_mass V) .: {(union S1)} by RELAT_1:def 16 ;
then A52: A1 \ {Bu} = (((center_of_mass V) | the topology of Kas) .: S1) \ ((center_of_mass V) .: {(union S1)}) by A33, A7, RELAT_1:129
.= (((center_of_mass V) | the topology of Kas) .: S1) \ (((center_of_mass V) | the topology of Kas) .: {(union S1)}) by A33, A36, RELAT_1:129, XBOOLE_1:1
.= ((center_of_mass V) | the topology of Kas) .: (S1 \ {(union S1)}) by FUNCT_1:64
.= (center_of_mass V) .: (S1 \ {(union S1)}) by A35, A33, RELAT_1:129, XBOOLE_1:1 ;
then conv ((@ A1) \ {Bu}) c= conv (union S1U) by CONVEX1:30, RLAFFIN2:17;
then A53: p1 in conv (union S1U) by A48;
card (union s2u) < n + 1 by A19, A39, CARD_2:48;
then A54: card (union s2u) <= n by NAT_1:13;
A55: union s1u c= union S1 by XBOOLE_1:36, ZFMISC_1:77;
A56: x in conv (@ A2) by A29, RLAFFIN2:def 1;
then A57: (x |-- (@ A2)) . Bu <= 1 by A3, RLAFFIN1:71;
A58: (x |-- (@ A2)) . Bu < 1

proof

assume (x |-- (@ A2)) . Bu >= 1 ; :: thesis:
then (x |-- (@ A2)) . Bu = 1 by A57, XXREAL_0:1;
hence contradiction by A3, A32, A56, RLAFFIN1:72; :: thesis:

end;

conv (@ A2) c= Affin (@ A2) by RLAFFIN1:65;
then A59: x = Sum (x |-- (@ A2)) by A3, A56, RLAFFIN1:def 7;
then Bu in Carrier (x |-- (@ A2)) by A3, A24, A29, A56, RLAFFIN1:71, RLAFFIN2:11;
then A60: (x |-- (@ A2)) . Bu <> 0 by RLVECT_2:19;
x |-- (@ A2) is convex by A3, A56, RLAFFIN1:71;
then consider p2 being Element of V such that
A61: p2 in conv ((@ A2) \ {Bu}) and
A62: x = (((x |-- (@ A2)) . Bu) * Bu) + ((1 - ((x |-- (@ A2)) . Bu)) * p2) and
((1 / ((x |-- (@ A2)) . Bu)) * x) + ((1 - (1 / ((x |-- (@ A2)) . Bu))) * p2) = Bu by A32, A59, A60, RLAFFIN2:1;
A63: p2 in Int ((@ A2) \ {Bu}) by A3, A24, A29, A61, A62, RLAFFIN2:14;
@ (union S1) is non empty finite Subset of V by A19;
then A64: Bu in Int (@ (union S1)) by A15, RLAFFIN2:20;
then A65: Bu in conv (@ (union S1)) by RLAFFIN2:def 1;
A66: S2 c= the topology of Kas

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A67: x in S2 ; :: thesis:
then reconsider A = x as Subset of Kas ;
A is simplex-like by A67, TOPS_2:def 1;
hence x in the topology of Kas ; :: thesis:

end;

union s1u <> union S1

proof

assume A68: union s1u = union S1 ; :: thesis:
then union s1u in s1u by A20, SIMPLEX0:9, ZFMISC_1:2;
hence contradiction by A68, ZFMISC_1:56; :: thesis:

end;

then A69: union s1u c< union S1 by A55;
then consider xS1U being object such that
A70: xS1U in @ (union S1) and
A71: not xS1U in union S1U by XBOOLE_0:6;
reconsider xS1U = xS1U as Element of V by A70;
union S1U c= (union S1) \ {xS1U} by A55, A71, ZFMISC_1:34;
then A72: conv (union S1U) c= conv (@ ((union S1) \ {xS1U})) by RLAFFIN1:3;
( (union S1) \ {xS1U} c= union S1 & (union S1) \ {xS1U} <> union S1 ) by A70, ZFMISC_1:56;
then (union S1) \ {xS1U} c< union S1 ;
then A73: not Bu in conv (@ ((union S1) \ {xS1U})) by A64, RLAFFIN2:def 1;
card (union s1u) < n + 1 by A19, A69, CARD_2:48;
then A74: card (union s1u) <= n by NAT_1:13;
( (union S1) \ {xS2U} c= union S1 & (union S1) \ {xS2U} <> union S1 ) by A40, ZFMISC_1:56;
then (union S1) \ {xS2U} c< union S1 ;
then A75: not Bu in conv (@ ((union S1) \ {xS2U})) by A64, RLAFFIN2:def 1;
A76: {(union S1)} c= S2 by A11, A18, A19, ZFMISC_1:2, ZFMISC_1:31;
A77: S2 \ {(union S1)} c= S2 by XBOOLE_1:36;
A78: A2 \ {Bu} = (((center_of_mass V) | the topology of Kas) .: S2) \ ((center_of_mass V) .: {(union S1)}) by A66, A8, A51, RELAT_1:129
.= (((center_of_mass V) | the topology of Kas) .: S2) \ (((center_of_mass V) | the topology of Kas) .: {(union S1)}) by A76, A66, RELAT_1:129, XBOOLE_1:1
.= ((center_of_mass V) | the topology of Kas) .: (S2 \ {(union S1)}) by FUNCT_1:64
.= (center_of_mass V) .: (S2 \ {(union S1)}) by A66, A77, RELAT_1:129, XBOOLE_1:1 ;
then conv ((@ A2) \ {Bu}) c= conv (union S2U) by CONVEX1:30, RLAFFIN2:17;
then A79: p2 in conv (union S2U) by A61;
x in conv (@ (union S1)) by A7, A17, A28, RLAFFIN2:def 1;
then p2 = p1 by A15, A45, A49, A58, A62, A65, A42, A53, A75, A72, A73, A79, RLAFFIN2:2;
then A80: Int ((@ A1) \ {Bu}) meets Int ((@ A2) \ {Bu}) by A50, A63, XBOOLE_0:3;
( (@ A1) \ {Bu} = @ (A1 \ {Bu}) & (@ A2) \ {Bu} = @ (A2 \ {Bu}) ) ;
then A1 \ {Bu} = A2 \ {Bu} by A6, A54, A52, A74, A78, A80;
hence A1 = (A2 \ {Bu}) \/ {Bu} by A22, ZFMISC_1:116
.= A2 by A24, ZFMISC_1:116 ;
:: thesis:

end;

A81: S₁[ 0 ]

proof

let S1, S2 be c=-linear finite simplex-like Subset-Family of Kas; :: thesis:
let A1, A2 be Simplex of (BCS Kas); :: thesis:
assume that
A82: A1 = (center_of_mass V) .: S1 and
A2 = (center_of_mass V) .: S2 and
A83: card (union S1) <= 0 and
card (union S2) <= 0 and
A84: Int (@ A1) meets Int (@ A2) ; :: thesis:
not Int (@ A1) is empty by A84;
then not A1 is empty ;
then consider y being object such that
A85: y in A1 ;
consider x being object such that
A86: x in dom (center_of_mass V) and
A87: x in S1 and
(center_of_mass V) . x = y by A82, A85, FUNCT_1:def 6;
reconsider xx = x as set by TARSKI:1;
A88: x <> {} by A86, ZFMISC_1:56;
union S1 is empty by A83;
then xx c= {} by A87, ZFMISC_1:74;
hence A1 = A2 by A88; :: thesis:

end;

A89: for n being Nat holds S₁[n] from NAT_1:sch 2(A81, A5);

now :: thesis:

let A1, A2 be Subset of (BCS Kas); :: thesis:
assume that
A90: A1 is simplex-like and
A91: A2 is simplex-like and
A92: Int (@ A1) meets Int (@ A2) ; :: thesis:
consider S1 being c=-linear finite simplex-like Subset-Family of Kas such that
A93: A1 = (center_of_mass V) .: S1 by A2, A90, SIMPLEX0:def 20;
consider S2 being c=-linear finite simplex-like Subset-Family of Kas such that
A94: A2 = (center_of_mass V) .: S2 by A2, A91, SIMPLEX0:def 20;
( card (union S1) <= card (union S2) or card (union S2) <= card (union S1) ) ;
hence A1 = A2 by A89, A90, A91, A92, A93, A94; :: thesis:

end;

hence BCS Kas is simplex-join-closed by Th25; :: thesis: