let n be Nat; :: thesis:
let V be RealLinearSpace; :: thesis:
let Aff be finite affinely-independent Subset of V; :: thesis:
let Bf be finite Subset of V; :: thesis:
let S be finite Subset-Family of V; :: thesis:
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:
set C = Complex_of {Aff};
reconsider c = card Aff as ExtReal ;
set BTC = (center_of_mass V) | 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 ((center_of_mass V),(Complex_of {Aff})) by Def5;
(card S) + n <= (card Aff) - 1 by A3, XREAL_1:19;
then A8: (card S) + n <= degree (BCS (Complex_of {Aff})) by A5, A6, Th31;

hereby :: thesis:

A9: S c= the topology of (Complex_of {Aff})

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume x in S ; :: thesis:
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:

end;

then A10: (center_of_mass V) .: S = ((center_of_mass V) | the topology of (Complex_of {Aff})) .: S by RELAT_1:129;
( dom (center_of_mass V) = (bool the carrier of V) \ {{}} & not {} in S ) by A1, FUNCT_2:def 1;
then ( dom ((center_of_mass V) | the topology of (Complex_of {Aff})) = (dom (center_of_mass V)) /\ the topology of (Complex_of {Aff}) & S c= dom (center_of_mass V) ) by RELAT_1:61, ZFMISC_1:34;
then A11: S c= dom ((center_of_mass V) | the topology of (Complex_of {Aff})) by A9, XBOOLE_1:19;
assume that
A12: Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) and
A13: (center_of_mass V) .: S c= Bf ; :: thesis:
consider a being c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) such that
A14: Bf = (center_of_mass V) .: a by A7, A12, SIMPLEX0:def 20;
a /\ (dom (center_of_mass V)) c= a by XBOOLE_1:17;
then reconsider AA = a /\ (dom (center_of_mass V)) as c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) by TOPS_2:11, XBOOLE_1:1;
A15: (center_of_mass V) .: S c= (center_of_mass V) .: AA by A13, A14, RELAT_1:112;
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 = ((center_of_mass V) | the topology of (Complex_of {Aff})) .: AA by RELAT_1:129;
A18: S \/ T = AA \/ S by XBOOLE_1:39
.= AA by A10, A11, A15, A17, FUNCT_1:87, XBOOLE_1:12 ;
T c= AA by XBOOLE_1:36;
then A19: T c= bool Aff by A4, A16;
A20: not {} in AA by ZFMISC_1:56;
then ( (center_of_mass V) .: a = (center_of_mass V) .: (a /\ (dom (center_of_mass V))) & AA is with_non-empty_elements ) by RELAT_1:112;
then A21: card Bf = card AA by A14, Th33;
A22: Bf = (center_of_mass V) .: AA by A14, RELAT_1:112
.= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A18, RELAT_1:120 ;
reconsider T = T as finite Subset-Family of V ;
take T = T; :: thesis:
card Bf = c + 1 by A8, A12, SIMPLEX0:def 18
.= ((card S) + n) + 1 by XXREAL_3:def 2 ;
then ( union (bool Aff) = Aff & (card S) + (card (AA \ S)) = ((card S) + n) + 1 ) by A18, A21, CARD_2:40, XBOOLE_1:79, ZFMISC_1:81;
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 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) by A18, A19, A20, A22, XBOOLE_1:79, ZFMISC_1:77; :: thesis:

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 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ; :: thesis:
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 A23, CARD_2:40
.= ((card S) + n) + 1 by A25 ;
union (T \/ S) = (union T) \/ (union S) by ZFMISC_1:78;
then union (T \/ S) c= Aff by A2, A26, XBOOLE_1:8;
then ( T \/ S c= bool (union (T \/ S)) & bool (union (T \/ S)) c= bool Aff ) by ZFMISC_1:67, ZFMISC_1:82;
then A29: T \/ S c= the topology of (Complex_of {Aff}) by A4;
A30: TS is simplex-like

let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis:
thus ( not a in TS or not a is dependent ) by A29; :: thesis:

end;

[#] (BCS (Complex_of {Aff})) = [#] (Complex_of {Aff}) by A7, SIMPLEX0:def 20;
then reconsider BTS = (center_of_mass V) .: TS as Simplex of (BCS (Complex_of {Aff})) by A7, A24, A30, SIMPLEX0:def 20;
card TS = card ((center_of_mass V) .: TS) by A24, A30, Th33;
then A31: card BTS = c + 1 by A28, XXREAL_3:def 2;
BTS = Bf by A27, RELAT_1:120;
hence ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) by A8, A27, A31, SIMPLEX0:def 18, XBOOLE_1:7; :: thesis: