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

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