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 by SIMPLEX0:def 7;
let A be Subset of K; :: 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 A in the topology of K by PRE_TOPC:def 5;
then A is empty by A1, SETFAM_1:def 11;
hence @ A is affinely-independent ; :: thesis: verum