let K be SimplicialComplexStr of V; :: thesis: ( K is empty-membered implies K is affinely-independent )
assume K is empty-membered ; :: thesis: K is affinely-independent
then A1: the topology of K is empty-membered ;
let A be Subset of K; :: 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 A in the topology of K ;
then A is empty by A1;
hence @ A is affinely-independent ; :: thesis: verum