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

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