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 & () .: 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 = (() .: Sk) \/ (() .: 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 & () .: 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 = (() .: Sk) \/ (() .: 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 & () .: 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 = (() .: Sk) \/ (() .: 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 & () .: 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 = (() .: Sk) \/ (() .: 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 & () .: 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 = (() .: Sk) \/ (() .: 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 & () .: 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 = (() .: Sk) \/ (() .: 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 ((),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 = (() .: Sk) \/ (() .: Tk) ) implies ( Af is Simplex of n + (card Sk), BCS K & () .: 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 = (() .: Sk) \/ (() .: R) )

consider T being c=-linear finite simplex-like Subset-Family of K such that
A10: Af = () .: T by ;
( union T is empty or union T in T ) by ;
then A11: union T is simplex-like by TOPS_2:def 1;
then @ () 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 ;
then reconsider s1 = Af as Simplex of (BCS ()) by ;
card Af = nc + 1 by ;
then A12: s1 is Simplex of n + (card Sk), BCS () by ;
set C = Complex_of {UT};
reconsider cT = card UT as ExtReal ;
|.().| c= [#] () ;
then A13: degree () = degree (BCS ()) by Th31;
( degree () = cT - 1 & card s1 <= (degree (BCS ())) + 1 ) by ;
then card s1 <= card UT by ;
then nc + 1 <= card UT by ;
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 ;
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 = (() .: Sk) \/ (() .: R) by A1, A9, A12, A14, Th35;
reconsider R = R as Subset-Family of K by A4;
( R c= bool () & bool () c= bool UT ) by ;
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 = (() .: Sk) \/ (() .: R) )
thus ( R misses Sk & R \/ Sk is c=-linear & R \/ Sk is with_non-empty_elements & card R = n + 1 & Af = (() .: Sk) \/ (() .: R) ) by ; :: thesis: verum
end;
given T being finite simplex-like Subset-Family of K such that A19: T misses Sk and
A20: ( T \/ Sk is c=-linear & T \/ Sk is with_non-empty_elements ) and
A21: card T = n + 1 and
A22: Af = (() .: Sk) \/ (() .: T) ; :: thesis: ( Af is Simplex of n + (card Sk), BCS K & () .: Sk c= Af )
set ST = Sk \/ T;
[#] K = [#] (BCS K) by ;
then reconsider BST = () .: (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 ;
card (Sk \/ T) = (card Sk) + (card T) by ;
then card BST = ((card Sk) + n) + 1 by ;
then ( ((center_of_mass V) .: Sk) \/ (() .: T) = () .: (Sk \/ T) & card BST = nc + 1 ) by ;
hence ( Af is Simplex of n + (card Sk), BCS K & () .: Sk c= Af ) by ; :: thesis: verum