let n be Nat; :: thesis: for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for Bf being finite Subset of V
for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) )

let V be RealLinearSpace; :: thesis: for Aff being finite affinely-independent Subset of V
for Bf being finite Subset of V
for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for Bf being finite Subset of V
for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) )

let Bf be finite Subset of V; :: thesis: for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) )

let S be finite Subset-Family of V; :: thesis: ( S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff implies ( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) ) )

set B = center_of_mass V;
set U = union S;
assume that
A1: S is with_non-empty_elements and
A2: union S c= Aff and
A3: ((card S) + n) + 1 <= card Aff ; :: thesis: ( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) )

set C = Complex_of {Aff};
reconsider c = card Aff as ExtReal ;
set BTC = () | the topology of (Complex_of {Aff});
set BC = BCS (Complex_of {Aff});
A4: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;
A5: degree (Complex_of {Aff}) = c - 1 by SIMPLEX0:26
.= (card Aff) + (- 1) by XXREAL_3:def 2 ;
reconsider c = (card S) + n as ExtReal ;
A6: |.(Complex_of {Aff}).| c= [#] (Complex_of {Aff}) ;
then A7: BCS (Complex_of {Aff}) = subdivision ((),(Complex_of {Aff})) by Def5;
(card S) + n <= (card Aff) - 1 by ;
then A8: (card S) + n <= degree (BCS (Complex_of {Aff})) by A5, A6, Th31;
hereby :: thesis: ( ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) implies ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) )
A9: S c= the topology of (Complex_of {Aff})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in the topology of (Complex_of {Aff}) )
reconsider xx = x as set by TARSKI:1;
assume x in S ; :: thesis: x in the topology of (Complex_of {Aff})
then xx c= union S by ZFMISC_1:74;
then xx c= Aff by A2;
hence x in the topology of (Complex_of {Aff}) by A4; :: thesis: verum
end;
then A10: (center_of_mass V) .: S = (() | the topology of (Complex_of {Aff})) .: S by RELAT_1:129;
( dom () = (bool the carrier of V) \ & not {} in S ) by ;
then ( dom (() | the topology of (Complex_of {Aff})) = () /\ the topology of (Complex_of {Aff}) & S c= dom () ) by ;
then A11: S c= dom (() | the topology of (Complex_of {Aff})) by ;
assume that
A12: Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) and
A13: (center_of_mass V) .: S c= Bf ; :: thesis: ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) )

consider a being c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) such that
A14: Bf = () .: a by ;
a /\ () c= a by XBOOLE_1:17;
then reconsider AA = a /\ () as c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) by ;
A15: (center_of_mass V) .: S c= () .: AA by ;
reconsider T = AA \ S as Subset-Family of V ;
A16: AA c= the topology of (Complex_of {Aff}) by SIMPLEX0:14;
then A17: (center_of_mass V) .: AA = (() | the topology of (Complex_of {Aff})) .: AA by RELAT_1:129;
A18: S \/ T = AA \/ S by XBOOLE_1:39
.= AA by ;
T c= AA by XBOOLE_1:36;
then A19: T c= bool Aff by ;
A20: not {} in AA by ZFMISC_1:56;
then ( (center_of_mass V) .: a = () .: (a /\ ()) & AA is with_non-empty_elements ) by RELAT_1:112;
then A21: card Bf = card AA by ;
A22: Bf = () .: AA by
.= (() .: S) \/ (() .: T) by ;
reconsider T = T as finite Subset-Family of V ;
take T = T; :: thesis: ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) )
card Bf = c + 1 by
.= ((card S) + n) + 1 by XXREAL_3:def 2 ;
then ( union (bool Aff) = Aff & (card S) + (card (AA \ S)) = ((card S) + n) + 1 ) by ;
hence ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = (() .: S) \/ (() .: T) ) by ; :: thesis: verum
end;
given T being finite Subset-Family of V such that A23: T misses S and
A24: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and
A25: card T = n + 1 and
A26: union T c= Aff and
A27: Bf = (() .: S) \/ (() .: T) ; :: thesis: ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf )
reconsider TS = T \/ S as Subset-Family of (Complex_of {Aff}) ;
reconsider t = T as finite Subset-Family of V ;
A28: card TS = (card t) + (card S) by
.= ((card S) + n) + 1 by A25 ;
union (T \/ S) = () \/ () by ZFMISC_1:78;
then union (T \/ S) c= Aff by ;
then ( T \/ S c= bool (union (T \/ S)) & bool (union (T \/ S)) c= bool Aff ) by ;
then A29: T \/ S c= the topology of (Complex_of {Aff}) by A4;
A30: TS is simplex-like
proof
let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in TS or not a is dependent )
thus ( not a in TS or not a is dependent ) by A29; :: thesis: verum
end;
[#] (BCS (Complex_of {Aff})) = [#] (Complex_of {Aff}) by ;
then reconsider BTS = () .: TS as Simplex of (BCS (Complex_of {Aff})) by ;
card TS = card (() .: TS) by ;
then A31: card BTS = c + 1 by ;
BTS = Bf by ;
hence ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & () .: S c= Bf ) by ; :: thesis: verum