let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Aff being finite affinely-independent Subset of V
for B being Subset of V st Aff is Simplex of K holds
( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Aff being finite affinely-independent Subset of V
for B being Subset of V st Aff is Simplex of K holds
( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )
let Aff be finite affinely-independent Subset of V; :: thesis: for B being Subset of V st Aff is Simplex of K holds
( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )
let B be Subset of V; :: thesis: ( Aff is Simplex of K implies ( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) ) )
set Bag = center_of_mass V;
set C = Complex_of {Aff};
A1: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;
assume Aff is Simplex of K ; :: thesis: ( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )
then reconsider s = Aff as Simplex of K ;
A2: [#] K = the carrier of V by SIMPLEX0:def 10;
then |.K.| c= [#] K ;
then A3: subdivision ((center_of_mass V),K) = BCS K by Def5;
@ s is affinely-independent ;
then A4: Complex_of {Aff} is SubSimplicialComplex of K by Th3;
then the topology of (Complex_of {Aff}) c= the topology of K by SIMPLEX0:def 13;
then A5: |.(Complex_of {Aff}).| c= |.K.| by Th4;
[#] (Complex_of {Aff}) = [#] V ;
then A6: subdivision ((center_of_mass V),(Complex_of {Aff})) = BCS (Complex_of {Aff}) by A5, Def5;
then BCS (Complex_of {Aff}) is SubSimplicialComplex of BCS K by A3, A4, SIMPLEX0:58;
then A7: the topology of (BCS (Complex_of {Aff})) c= the topology of (BCS K) by SIMPLEX0:def 13;

hereby :: thesis: ( B is Simplex of (BCS K) & conv B c= conv Aff implies B is Simplex of (BCS (Complex_of {Aff})) )

assume B is Simplex of (BCS (Complex_of {Aff})) ; :: thesis: ( B is Simplex of (BCS K) & conv B c= conv Aff )
then reconsider A = B as Simplex of (BCS (Complex_of {Aff})) ;
A in the topology of (BCS (Complex_of {Aff})) by PRE_TOPC:def 2;
then A in the topology of (BCS K) by A7;
then reconsider a = A as Simplex of (BCS K) by PRE_TOPC:def 2;
( |.(BCS (Complex_of {Aff})).| = |.(Complex_of {Aff}).| & conv (@ A) c= |.(BCS (Complex_of {Aff})).| ) by Th5, Th10;
then conv (@ a) c= conv Aff by Th8;
hence ( B is Simplex of (BCS K) & conv B c= conv Aff ) ; :: thesis: verum

end;

assume that
A8: B is Simplex of (BCS K) and
A9: conv B c= conv Aff ; :: thesis: B is Simplex of (BCS (Complex_of {Aff}))
reconsider A = B as Simplex of (BCS K) by A8;
consider SS being c=-linear finite simplex-like Subset-Family of K such that
A10: B = (center_of_mass V) .: SS by A3, A8, SIMPLEX0:def 20;
reconsider ss = SS as c=-linear finite Subset-Family of (Complex_of {Aff}) by A2;
[#] (subdivision ((center_of_mass V),(Complex_of {Aff}))) = [#] (Complex_of {Aff}) by SIMPLEX0:def 20;
then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {Aff})) by A5, Def5;
A11: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;
ss is simplex-like

proof

let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in ss or not a is dependent )
assume A12: a in ss ; :: thesis: not a is dependent
reconsider aK = a as Simplex of K by A12, TOPS_2:def 1;

per cases ( aK is empty or not aK is empty ) ;

suppose aK is empty ; :: thesis: not a is dependent

hence not a is dependent ; :: thesis: verum

end;

suppose A13: not aK is empty ; :: thesis: not a is dependent

then aK in dom (center_of_mass V) by A11, ZFMISC_1:56;
then A14: (center_of_mass V) . aK in A by A10, A12, FUNCT_1:def 6;
A15: (center_of_mass V) . aK in Int (@ aK) by A13, RLAFFIN2:20;
A c= conv (@ A) by RLAFFIN1:2;
then (center_of_mass V) . aK in conv (@ A) by A14;
then Int (@ aK) meets conv (@ s) by A9, A15, XBOOLE_0:3;
then aK c= Aff by Th26;
hence not a is dependent by A1; :: thesis: verum

end;

end;

end;

then Bss is simplex-like by A6, SIMPLEX0:def 20;
hence B is Simplex of (BCS (Complex_of {Aff})) by A10; :: thesis: verum