let S be SubSimplicialComplex of K; :: thesis: S is affinely-independent
let A be Subset of S; :: according to SIMPLEX1:def 7 :: thesis: ( A is simplex-like implies @ A is affinely-independent )
assume A is simplex-like ; :: thesis: @ A is affinely-independent
then A1: A in the topology of S ;
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 ;
A1 is simplex-like by A1, A2;
then @ A1 is affinely-independent by Def7;
hence @ A is affinely-independent ; :: thesis: verum