let X be set ; :: thesis: for n, k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let n, k be Nat; :: thesis: for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let V be RealLinearSpace; :: thesis: for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let Aff be finite affinely-independent Subset of V; :: thesis: for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let S be Simplex of n - 1, BCS (k,(Complex_of {Aff})); :: thesis: ( card Aff = n + 1 & X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } implies ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
assume A1: card Aff = n + 1 ; :: thesis: ( not X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } or ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
set C = Complex_of {Aff};
reconsider cA = card Aff as ExtReal ;
A2: cA - 1 = (card Aff) + (- 1) by XXREAL_3:def 2
.= n by A1 ;
then A3: degree (Complex_of {Aff}) = n by SIMPLEX0:26;
defpred S₁[ Nat] means for S being Simplex of n - 1, BCS ($1,(Complex_of {Aff}))
for X being set st X = { S1 where S1 is Simplex of n, BCS ($1,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) );
A4: ( [#] (Complex_of {Aff}) = [#] V & |.(Complex_of {Aff}).| c= [#] V ) ;
A5: S₁[ 0 ]

proof

reconsider n1 = n - 1 as ExtReal ;
A6: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;
Aff in bool Aff by ZFMISC_1:def 1;
then reconsider A1 = Aff as finite Simplex of (Complex_of {Aff}) by A6, PRE_TOPC:def 2;
A7: BCS (0,(Complex_of {Aff})) = Complex_of {Aff} by A4, Th16;
let S be Simplex of n - 1, BCS (0,(Complex_of {Aff})); :: thesis: for X being set st X = { S1 where S1 is Simplex of n, BCS (0,(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let X be set ; :: thesis: ( X = { S1 where S1 is Simplex of n, BCS (0,(Complex_of {Aff})) : S c= S1 } implies ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
assume A8: X = { S1 where S1 is Simplex of n, BCS (0,(Complex_of {Aff})) : S c= S1 } ; :: thesis: ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
A9: X c= {Aff}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {Aff} )
reconsider N = n as ExtReal ;
assume x in X ; :: thesis: x in {Aff}
then consider U being Simplex of n, Complex_of {Aff} such that
A10: x = U and
S c= U by A7, A8;
A11: U in the topology of (Complex_of {Aff}) by PRE_TOPC:def 2;
card U = N + 1 by A3, SIMPLEX0:def 18
.= n + 1 by XXREAL_3:def 2 ;
then Aff = U by A1, A6, A11, CARD_2:102;
hence x in {Aff} by A10, TARSKI:def 1; :: thesis: verum

end;

A12: S in bool Aff by A6, A7, PRE_TOPC:def 2;
A1 is Simplex of n, Complex_of {Aff} by A2, SIMPLEX0:48;
then Aff in X by A7, A8, A12;
then A13: X = {Aff} by A9, ZFMISC_1:33;
( n + (- 1) >= - 1 & n - 1 <= degree (Complex_of {Aff}) ) by A3, XREAL_1:31, XREAL_1:146;
then card S = n1 + 1 by A7, SIMPLEX0:def 18
.= (n - 1) + 1 by XXREAL_3:def 2 ;
then S <> Aff by A1;
then S c< Aff by A12;
hence ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) by A13, CARD_1:30, RLAFFIN2:7; :: thesis: verum

end;

A14: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A15: S₁[k] ; :: thesis: S₁[k + 1]
A16: ( degree (BCS (k,(Complex_of {Aff}))) = n & BCS ((k + 1),(Complex_of {Aff})) = BCS (BCS (k,(Complex_of {Aff}))) ) by A3, A4, Th20, Th32;
let S be Simplex of n - 1, BCS ((k + 1),(Complex_of {Aff})); :: thesis: for X being set st X = { S1 where S1 is Simplex of n, BCS ((k + 1),(Complex_of {Aff})) : S c= S1 } holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
let X be set ; :: thesis: ( X = { S1 where S1 is Simplex of n, BCS ((k + 1),(Complex_of {Aff})) : S c= S1 } implies ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) )
assume A17: X = { S1 where S1 is Simplex of n, BCS ((k + 1),(Complex_of {Aff})) : S c= S1 } ; :: thesis: ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
thus ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) by A1, A15, A16, A17, Th44; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A14);
hence ( not X = { S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1 } or ( ( conv (@ S) meets Int Aff implies card X = 2 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) ) ) ; :: thesis: verum