let n be Nat; :: thesis: for V being RealLinearSpace

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let Af be finite Subset of V; :: thesis: for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let Sk be finite simplex-like Subset-Family of K; :: thesis: ( Sk is with_non-empty_elements & (card Sk) + n <= degree K implies ( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) ) )

set B = center_of_mass V;

set BK = BCS K;

assume that

A1: Sk is with_non-empty_elements and

A2: (card Sk) + n <= degree K ; :: thesis: ( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

reconsider nc = n + (card Sk) as ExtReal ;

A3: (nc + 1) - 1 = nc by XXREAL_3:22;

A4: [#] K = the carrier of V by SIMPLEX0:def 10;

then A5: |.K.| c= [#] K ;

then A6: subdivision ((center_of_mass V),K) = BCS K by Def5;

A7: nc <= degree (BCS K) by A2, A5, Th31;

A20: ( T \/ Sk is c=-linear & T \/ Sk is with_non-empty_elements ) and

A21: card T = n + 1 and

A22: Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: T) ; :: thesis: ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af )

set ST = Sk \/ T;

[#] K = [#] (BCS K) by A6, SIMPLEX0:def 20;

then reconsider BST = (center_of_mass V) .: (Sk \/ T) as Subset of (BCS K) by SIMPLEX0:def 10;

A23: Sk \/ T is simplex-like by TOPS_2:13;

then reconsider BST = BST as Simplex of (BCS K) by A6, A20, SIMPLEX0:def 20;

card (Sk \/ T) = (card Sk) + (card T) by A19, CARD_2:40;

then card BST = ((card Sk) + n) + 1 by A20, A21, A23, Th33;

then ( ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: T) = (center_of_mass V) .: (Sk \/ T) & card BST = nc + 1 ) by RELAT_1:120, XXREAL_3:def 2;

hence ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) by A3, A22, SIMPLEX0:48, XBOOLE_1:7; :: thesis: verum

for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Af being finite Subset of V

for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let Af be finite Subset of V; :: thesis: for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements & (card Sk) + n <= degree K holds

( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

let Sk be finite simplex-like Subset-Family of K; :: thesis: ( Sk is with_non-empty_elements & (card Sk) + n <= degree K implies ( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) ) )

set B = center_of_mass V;

set BK = BCS K;

assume that

A1: Sk is with_non-empty_elements and

A2: (card Sk) + n <= degree K ; :: thesis: ( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )

reconsider nc = n + (card Sk) as ExtReal ;

A3: (nc + 1) - 1 = nc by XXREAL_3:22;

A4: [#] K = the carrier of V by SIMPLEX0:def 10;

then A5: |.K.| c= [#] K ;

then A6: subdivision ((center_of_mass V),K) = BCS K by Def5;

A7: nc <= degree (BCS K) by A2, A5, Th31;

hereby :: thesis: ( ex Tk being finite simplex-like Subset-Family of K st

( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) implies ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) )

given T being finite simplex-like Subset-Family of K such that A19:
T misses Sk
and ( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) implies ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) )

assume that

A8: Af is Simplex of n + (card Sk), BCS K and

A9: (center_of_mass V) .: Sk c= Af ; :: thesis: ex R being finite simplex-like Subset-Family of K st

( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) )

consider T being c=-linear finite simplex-like Subset-Family of K such that

A10: Af = (center_of_mass V) .: T by A6, A8, SIMPLEX0:def 20;

( union T is empty or union T in T ) by SIMPLEX0:9, ZFMISC_1:2;

then A11: union T is simplex-like by TOPS_2:def 1;

then @ (union T) is affinely-independent ;

then reconsider UT = union T as finite affinely-independent Subset of V ;

UT = union (@ T) ;

then conv Af c= conv UT by A10, CONVEX1:30, RLAFFIN2:17;

then reconsider s1 = Af as Simplex of (BCS (Complex_of {UT})) by A8, A11, Th40;

card Af = nc + 1 by A7, A8, SIMPLEX0:def 18;

then A12: s1 is Simplex of n + (card Sk), BCS (Complex_of {UT}) by A3, SIMPLEX0:48;

set C = Complex_of {UT};

reconsider cT = card UT as ExtReal ;

|.(Complex_of {UT}).| c= [#] (Complex_of {UT}) ;

then A13: degree (Complex_of {UT}) = degree (BCS (Complex_of {UT})) by Th31;

( degree (Complex_of {UT}) = cT - 1 & card s1 <= (degree (BCS (Complex_of {UT}))) + 1 ) by SIMPLEX0:24, SIMPLEX0:26;

then card s1 <= card UT by A13, XXREAL_3:22;

then nc + 1 <= card UT by A7, A8, SIMPLEX0:def 18;

then A14: ((card Sk) + n) + 1 <= card UT by XXREAL_3:def 2;

( the_family_of K is subset-closed & UT in the topology of K ) by A11;

then A15: bool UT c= the topology of K by SIMPLEX0:1;

union (@ Sk) c= union T by A1, A5, A8, A9, A10, Th34, ZFMISC_1:77;

then consider R being finite Subset-Family of V such that

A16: ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 ) and

A17: union R c= UT and

A18: Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) by A1, A9, A12, A14, Th35;

reconsider R = R as Subset-Family of K by A4;

( R c= bool (union R) & bool (union R) c= bool UT ) by A17, SIMPLEX0:1, ZFMISC_1:82;

then R c= bool UT ;

then R c= the topology of K by A15;

then reconsider R = R as finite simplex-like Subset-Family of K by SIMPLEX0:14;

take R = R; :: thesis: ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) )

thus ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) ) by A16, A18; :: thesis: verum

end;A8: Af is Simplex of n + (card Sk), BCS K and

A9: (center_of_mass V) .: Sk c= Af ; :: thesis: ex R being finite simplex-like Subset-Family of K st

( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) )

consider T being c=-linear finite simplex-like Subset-Family of K such that

A10: Af = (center_of_mass V) .: T by A6, A8, SIMPLEX0:def 20;

( union T is empty or union T in T ) by SIMPLEX0:9, ZFMISC_1:2;

then A11: union T is simplex-like by TOPS_2:def 1;

then @ (union T) is affinely-independent ;

then reconsider UT = union T as finite affinely-independent Subset of V ;

UT = union (@ T) ;

then conv Af c= conv UT by A10, CONVEX1:30, RLAFFIN2:17;

then reconsider s1 = Af as Simplex of (BCS (Complex_of {UT})) by A8, A11, Th40;

card Af = nc + 1 by A7, A8, SIMPLEX0:def 18;

then A12: s1 is Simplex of n + (card Sk), BCS (Complex_of {UT}) by A3, SIMPLEX0:48;

set C = Complex_of {UT};

reconsider cT = card UT as ExtReal ;

|.(Complex_of {UT}).| c= [#] (Complex_of {UT}) ;

then A13: degree (Complex_of {UT}) = degree (BCS (Complex_of {UT})) by Th31;

( degree (Complex_of {UT}) = cT - 1 & card s1 <= (degree (BCS (Complex_of {UT}))) + 1 ) by SIMPLEX0:24, SIMPLEX0:26;

then card s1 <= card UT by A13, XXREAL_3:22;

then nc + 1 <= card UT by A7, A8, SIMPLEX0:def 18;

then A14: ((card Sk) + n) + 1 <= card UT by XXREAL_3:def 2;

( the_family_of K is subset-closed & UT in the topology of K ) by A11;

then A15: bool UT c= the topology of K by SIMPLEX0:1;

union (@ Sk) c= union T by A1, A5, A8, A9, A10, Th34, ZFMISC_1:77;

then consider R being finite Subset-Family of V such that

A16: ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 ) and

A17: union R c= UT and

A18: Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) by A1, A9, A12, A14, Th35;

reconsider R = R as Subset-Family of K by A4;

( R c= bool (union R) & bool (union R) c= bool UT ) by A17, SIMPLEX0:1, ZFMISC_1:82;

then R c= bool UT ;

then R c= the topology of K by A15;

then reconsider R = R as finite simplex-like Subset-Family of K by SIMPLEX0:14;

take R = R; :: thesis: ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) )

thus ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: R) ) by A16, A18; :: thesis: verum

A20: ( T \/ Sk is c=-linear & T \/ Sk is with_non-empty_elements ) and

A21: card T = n + 1 and

A22: Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: T) ; :: thesis: ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af )

set ST = Sk \/ T;

[#] K = [#] (BCS K) by A6, SIMPLEX0:def 20;

then reconsider BST = (center_of_mass V) .: (Sk \/ T) as Subset of (BCS K) by SIMPLEX0:def 10;

A23: Sk \/ T is simplex-like by TOPS_2:13;

then reconsider BST = BST as Simplex of (BCS K) by A6, A20, SIMPLEX0:def 20;

card (Sk \/ T) = (card Sk) + (card T) by A19, CARD_2:40;

then card BST = ((card Sk) + n) + 1 by A20, A21, A23, Th33;

then ( ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: T) = (center_of_mass V) .: (Sk \/ T) & card BST = nc + 1 ) by RELAT_1:120, XXREAL_3:def 2;

hence ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) by A3, A22, SIMPLEX0:48, XBOOLE_1:7; :: thesis: verum