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_{1} being set holds

( not x in S2 or not b_{1} in S2 or x,b_{1} 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;

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

( not x in S2 or not b

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 ) )
;

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;hence x,y are_c=-comparable by ORDINAL1:def 8; :: thesis: verum