let V be RealLinearSpace; :: thesis: for Aff being finite affinely-independent Subset of V
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )

let Sf be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( Sf is with_non-empty_elements & union Sf c= Aff implies ( () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) )

reconsider N = 0 as Nat ;
set U = union Sf;
assume that
A1: Sf is with_non-empty_elements and
A2: union Sf c= Aff ; :: thesis: ( () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )

set B = center_of_mass V;
set C = Complex_of {Aff};
reconsider s = Sf as c=-linear finite Subset-Family of (Complex_of {Aff}) ;
A3: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;
Segm (card (union Sf)) c= Segm (card Aff) by ;
then card (union Sf) <= card Aff by NAT_1:39;
then A4: ( N - 1 <= (card (union Sf)) - 1 & (card (union Sf)) - 1 <= (card Aff) - 1 ) by XREAL_1:9;
( Sf c= bool (union Sf) & bool (union Sf) c= bool Aff ) by ;
then A5: s c= the topology of (Complex_of {Aff}) by A3;
A6: s is simplex-like
proof
let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in s or not a is dependent )
assume a in s ; :: thesis: not a is dependent
hence not a is dependent by A5; :: thesis: verum
end;
then A7: card s = card (() .: Sf) by ;
Segm (card Sf) c= Segm (card (union Sf)) by ;
then A8: card Sf <= card (union Sf) by NAT_1:39;
set BC = BCS (Complex_of {Aff});
reconsider c = card Aff as ExtReal ;
A9: degree (Complex_of {Aff}) = c - 1 by SIMPLEX0:26
.= (card Aff) + (- 1) by XXREAL_3:def 2 ;
A10: |.(Complex_of {Aff}).| c= [#] (Complex_of {Aff}) ;
then A11: BCS (Complex_of {Aff}) = subdivision ((),(Complex_of {Aff})) by Def5;
then [#] (BCS (Complex_of {Aff})) = [#] (Complex_of {Aff}) by SIMPLEX0:def 20;
then reconsider BS = () .: Sf as Subset of (BCS (Complex_of {Aff})) ;
A12: N - 1 <= (card Aff) - 1 by XREAL_1:9;
A13: degree (BCS (Complex_of {Aff})) = degree (Complex_of {Aff}) by ;
thus ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) implies for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) :: thesis: ( ( for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) implies () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) )
proof
assume (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) ; :: thesis: for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n )

then reconsider BS = () .: Sf as Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) ;
reconsider c1 = (card (union Sf)) - 1 as ExtReal ;
let n be Nat; :: thesis: ( 0 < n & n <= card (union Sf) implies ex x being set st
( x in Sf & card x = n ) )

reconsider s = Sf as Subset-Family of (union Sf) by ZFMISC_1:82;
defpred S1[ Nat] means ( \$1 < card Sf implies ex x being finite set st
( x in Sf & card x = (card Sf) - \$1 ) );
assume that
A14: 0 < n and
A15: n <= card (union Sf) ; :: thesis: ex x being set st
( x in Sf & card x = n )

A16: (card Sf) - 0 > (card Sf) - n by ;
A17: card BS = c1 + 1 by
.= ((card (union Sf)) - 1) + 1 by XXREAL_3:def 2
.= card (union Sf) ;
then A18: not Sf is empty by ;
then consider s1 being Subset-Family of (union Sf) such that
A19: s c= s1 and
( s1 is with_non-empty_elements & s1 is c=-linear ) and
A20: card (union Sf) = card s1 and
A21: for Z being set st Z in s1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in s1 ) by ;
card (union Sf) = card Sf by A1, A6, A17, Th33;
then A22: s = s1 by ;
A23: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A24: S1[n] ; :: thesis: S1[n + 1]
assume A25: n + 1 < card Sf ; :: thesis: ex x being finite set st
( x in Sf & card x = (card Sf) - (n + 1) )

then consider X being finite set such that
A26: X in Sf and
A27: card X = (card Sf) - n by ;
A28: (n + 1) - n < (card Sf) - n by ;
then consider x being set such that
A29: ( x in X & X \ {x} in Sf ) by A21, A22, A26, A27;
reconsider C = (card X) - 1 as Element of NAT by ;
take X \ {x} ; :: thesis: ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) )
card X = C + 1 ;
hence ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) ) by ; :: thesis: verum
end;
A30: S1[ 0 ] by ;
A31: for n being Nat holds S1[n] from (card Sf) - n is Nat by ;
then ex x being finite set st
( x in Sf & card x = (card Sf) - ((card Sf) - n) ) by ;
hence ex x being set st
( x in Sf & card x = n ) ; :: thesis: verum
end;
assume A32: for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ; :: thesis: () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})
per cases ( union Sf is empty or not union Sf is empty ) ;
suppose A33: union Sf is empty ; :: thesis: () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})
reconsider O = - 1 as ExtReal ;
A34: ( O <= degree (BCS (Complex_of {Aff})) & 0 = O + 1 ) by ;
Sf is empty by ;
then A35: BS is empty ;
thus (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by ; :: thesis: verum
end;
suppose A36: not union Sf is empty ; :: thesis: () .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})
reconsider c1 = (card (union Sf)) - 1 as ExtReal ;
consider x being set such that
A37: x in Sf and
card x = card (union Sf) by ;
defpred S1[ object , object ] means ex D2 being set st
( D2 = \$2 & card D2 = \$1 );
A38: for x being object st x in Seg (card (union Sf)) holds
ex y being object st
( y in Sf & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Seg (card (union Sf)) implies ex y being object st
( y in Sf & S1[x,y] ) )

assume A39: x in Seg (card (union Sf)) ; :: thesis: ex y being object st
( y in Sf & S1[x,y] )

reconsider n = x as Nat by A39;
( 0 < n & n <= card (union Sf) ) by ;
then ex x being set st
( x in Sf & card x = n ) by A32;
hence ex y being object st
( y in Sf & S1[x,y] ) ; :: thesis: verum
end;
consider f being Function of (Seg (card (union Sf))),Sf such that
A40: for x being object st x in Seg (card (union Sf)) holds
S1[x,f . x] from
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A41: x1 in dom f and
A42: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
A43: S1[x2,f . x2] by ;
S1[x1,f . x1] by ;
hence x1 = card (f . x1)
.= x2 by ;
:: thesis: verum
end;
then A44: ( rng f c= Sf & f is one-to-one ) by FUNCT_1:def 4;
dom f = Seg (card (union Sf)) by ;
then ( Segm (card (Seg (card (union Sf)))) = Segm (card (union Sf)) & Segm (card (Seg (card (union Sf)))) c= Segm (card Sf) ) by ;
then card (union Sf) <= card Sf by NAT_1:39;
then A45: card BS = card (union Sf) by ;
( BS is Simplex of (BCS (Complex_of {Aff})) & c1 + 1 = ((card (union Sf)) - 1) + 1 ) by ;
hence (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by ; :: thesis: verum
end;
end;