let V be RealLinearSpace; :: thesis: 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 & () .: S2 is Simplex of (BCS Kas) & () .: S1 c= () .: S2 holds
( S1 c= S2 & S2 is c=-linear )

let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for S1, S2 being simplex-like Subset-Family of Kas st |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & () .: S2 is Simplex of (BCS Kas) & () .: S1 c= () .: 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; :: thesis: ( |.Kas.| c= [#] Kas & S1 is with_non-empty_elements & () .: S2 is Simplex of (BCS Kas) & () .: S1 c= () .: 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= () .: S2 ; :: thesis: ( S1 c= S2 & S2 is c=-linear )
BCS Kas = subdivision ((),Kas) by ;
then consider W2 being c=-linear finite simplex-like Subset-Family of Kas such that
A5: (center_of_mass V) .: S2 = () .: W2 by ;
reconsider s2 = S2 \ as simplex-like Subset-Family of Kas by ;
set TK = the topology of Kas;
set BTK = () | the topology of Kas;
A6: dom (() | the topology of Kas) = () /\ the topology of Kas by RELAT_1:61;
A7: s2 c= the topology of Kas by SIMPLEX0:14;
A8: dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
then (@ S2) \ c= dom () by XBOOLE_1:33;
then s2 c= () /\ the topology of Kas by ;
then A9: s2 c= dom (() | the topology of Kas) by RELAT_1:61;
W2 /\ () c= W2 by XBOOLE_1:17;
then reconsider w2 = W2 /\ () as c=-linear finite simplex-like Subset-Family of Kas by ;
A10: w2 c= the topology of Kas by SIMPLEX0:14;
then A11: ( (center_of_mass V) .: W2 = () .: (W2 /\ ()) & () .: w2 = (() | the topology of Kas) .: w2 ) by ;
W2 /\ () c= dom () by XBOOLE_1:17;
then A12: w2 c= dom (() | the topology of Kas) by ;
S2 c= the topology of Kas by SIMPLEX0:14;
then (center_of_mass V) .: S2 = (() | the topology of Kas) .: S2 by RELAT_1:129;
then A13: w2 c= S2 by ;
A14: S1 c= the topology of Kas by SIMPLEX0:14;
S2 /\ () = ((@ S2) /\ (bool the carrier of V)) \ by
.= s2 by XBOOLE_1:28 ;
then A15: (center_of_mass V) .: S2 = () .: s2 by RELAT_1:112;
then ((center_of_mass V) | the topology of Kas) .: s2 = () .: S2 by ;
then A16: s2 c= w2 by ;
( @ S1 c= bool the carrier of V & not {} in S1 ) by A2;
then S1 c= dom () by ;
then A17: S1 c= dom (() | the topology of Kas) by ;
(center_of_mass V) .: S1 = (() | the topology of Kas) .: S1 by ;
then S1 c= w2 by ;
hence S1 c= S2 by A13; :: thesis: S2 is c=-linear
let x be set ; :: according to ORDINAL1:def 8 :: thesis: for b1 being set holds
( not x in S2 or not b1 in S2 or x,b1 are_c=-comparable )

let y be set ; :: thesis: ( not x in S2 or not y in S2 or x,y are_c=-comparable )
assume A18: ( x in S2 & y in S2 ) ; :: thesis:
(center_of_mass V) .: s2 = (() | the topology of Kas) .: s2 by ;
then w2 c= s2 by ;
then A19: s2 = w2 by A16;
per cases ( x is empty or y is empty or ( not x is empty & not y is empty ) ) ;
end;