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_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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

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

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

proof

A14:
for k being Nat st S
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}

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;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

A12:
S in bool Aff
by A6, A7, PRE_TOPC:def 2;
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;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

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

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A15: S_{1}[k]
; :: thesis: S_{1}[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;assume A15: S

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

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