let S be SubSimplicialComplex of K; :: thesis: S is affinely-independent
let A be Subset of S; :: according to SIMPLEX1:def 7 :: thesis: ( not A is dependent implies @ A is affinely-independent )
assume not A is dependent ; :: thesis: @ A is affinely-independent
then A1: A in the topology of S by PRE_TOPC:def 5;
A2: the topology of S c= the topology of K by SIMPLEX0:def 13;
then A in the topology of K by A1;
then reconsider A1 = A as Subset of K ;
not A1 is dependent by A1, A2, PRE_TOPC:def 5;
then @ A1 is affinely-independent by Def7;
hence @ A is affinely-independent ; :: thesis: verum