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 & (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; :: thesis: 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; :: thesis: ( |.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 ; :: thesis: ( 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; :: thesis: S2 is c=-linear
let x be set ; :: according to ORDINAL1:def 8 :: thesis: for b₁ being set holds
( not x in S2 or not b₁ in S2 or x,b₁ 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: 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;

per cases ( x is empty or y is empty or ( not x is empty & not y is empty ) ) ;

suppose ( x is empty or y is empty ) ; :: thesis: x,y are_c=-comparable

then ( x c= y or y c= x ) ;
hence x,y are_c=-comparable ; :: thesis: verum

end;

suppose ( not x is empty & not y is empty ) ; :: thesis: x,y are_c=-comparable

then ( x in w2 & y in w2 ) by A18, A19, ZFMISC_1:56;
hence x,y are_c=-comparable by ORDINAL1:def 8; :: thesis: verum

end;

end;