let V be RealLinearSpace; for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V
for S1, S2 being simplex-like Subset-Family of Kas st |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & (center_of_mass V) .: S2 is Simplex of (BCS Kas) & (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 holds
( S1 c= S2 & S2 is c=-linear )
let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; for S1, S2 being simplex-like Subset-Family of Kas st |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & (center_of_mass V) .: S2 is Simplex of (BCS Kas) & (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 holds
( S1 c= S2 & S2 is c=-linear )
set B = center_of_mass V;
set BK = BCS Kas;
let S1, S2 be simplex-like Subset-Family of Kas; ( |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & (center_of_mass V) .: S2 is Simplex of (BCS Kas) & (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 implies ( S1 c= S2 & S2 is c=-linear ) )
assume that
A1:
|.Kas.| c= [#] Kas
and
A2:
S1 is with_non-empty_elements
and
A3:
(center_of_mass V) .: S2 is Simplex of (BCS Kas)
and
A4:
(center_of_mass V) .: S1 c= (center_of_mass V) .: S2
; ( S1 c= S2 & S2 is c=-linear )
BCS Kas = subdivision ((center_of_mass V),Kas)
by A1, Def5;
then consider W2 being c=-linear finite simplex-like Subset-Family of Kas such that
A5:
(center_of_mass V) .: S2 = (center_of_mass V) .: W2
by A3, SIMPLEX0:def 20;
reconsider s2 = S2 \ {{}} as simplex-like Subset-Family of Kas by TOPS_2:11, XBOOLE_1:36;
set TK = the topology of Kas;
set BTK = (center_of_mass V) | the topology of Kas;
A6:
dom ((center_of_mass V) | the topology of Kas) = (dom (center_of_mass V)) /\ the topology of Kas
by RELAT_1:61;
A7:
s2 c= the topology of Kas
by SIMPLEX0:14;
A8:
dom (center_of_mass V) = (bool the carrier of V) \ {{}}
by FUNCT_2:def 1;
then
(@ S2) \ {{}} c= dom (center_of_mass V)
by XBOOLE_1:33;
then
s2 c= (dom (center_of_mass V)) /\ the topology of Kas
by A7, XBOOLE_1:19;
then A9:
s2 c= dom ((center_of_mass V) | the topology of Kas)
by RELAT_1:61;
W2 /\ (dom (center_of_mass V)) c= W2
by XBOOLE_1:17;
then reconsider w2 = W2 /\ (dom (center_of_mass V)) as c=-linear finite simplex-like Subset-Family of Kas by TOPS_2:11, XBOOLE_1:1;
A10:
w2 c= the topology of Kas
by SIMPLEX0:14;
then A11:
( (center_of_mass V) .: W2 = (center_of_mass V) .: (W2 /\ (dom (center_of_mass V))) & (center_of_mass V) .: w2 = ((center_of_mass V) | the topology of Kas) .: w2 )
by RELAT_1:112, RELAT_1:129;
W2 /\ (dom (center_of_mass V)) c= dom (center_of_mass V)
by XBOOLE_1:17;
then A12:
w2 c= dom ((center_of_mass V) | the topology of Kas)
by A6, A10, XBOOLE_1:19;
S2 c= the topology of Kas
by SIMPLEX0:14;
then
(center_of_mass V) .: S2 = ((center_of_mass V) | the topology of Kas) .: S2
by RELAT_1:129;
then A13:
w2 c= S2
by A5, A11, A12, FUNCT_1:87;
A14:
S1 c= the topology of Kas
by SIMPLEX0:14;
S2 /\ (dom (center_of_mass V)) =
((@ S2) /\ (bool the carrier of V)) \ {{}}
by A8, XBOOLE_1:49
.=
s2
by XBOOLE_1:28
;
then A15:
(center_of_mass V) .: S2 = (center_of_mass V) .: s2
by RELAT_1:112;
then
((center_of_mass V) | the topology of Kas) .: s2 = (center_of_mass V) .: S2
by A7, RELAT_1:129;
then A16:
s2 c= w2
by A5, A11, A9, FUNCT_1:87;
( @ S1 c= bool the carrier of V & not {} in S1 )
by A2;
then
S1 c= dom (center_of_mass V)
by A8, ZFMISC_1:34;
then A17:
S1 c= dom ((center_of_mass V) | the topology of Kas)
by A6, A14, XBOOLE_1:19;
(center_of_mass V) .: S1 = ((center_of_mass V) | the topology of Kas) .: S1
by A14, RELAT_1:129;
then
S1 c= w2
by A4, A5, A11, A17, FUNCT_1:87;
hence
S1 c= S2
by A13; S2 is c=-linear
let x be set ; ORDINAL1:def 8 for b1 being set holds
( not x in S2 or not b1 in S2 or x,b1 are_c=-comparable )
let y be set ; ( not x in S2 or not y in S2 or x,y are_c=-comparable )
assume A18:
( x in S2 & y in S2 )
; x,y are_c=-comparable
(center_of_mass V) .: s2 = ((center_of_mass V) | the topology of Kas) .: s2
by A7, RELAT_1:129;
then
w2 c= s2
by A5, A11, A12, A15, FUNCT_1:87;
then A19:
s2 = w2
by A16;