let A be Subset of (Complex_of F); :: 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 subset-closed_closure_of F by PRE_TOPC:def 5;
then consider x being set such that
A2: A c= x and
A3: x in F by SIMPLEX0:2;
x is affinely-independent Subset of V by A3, RLAFFIN1:def 5;
hence @ A is affinely-independent by A2, RLAFFIN1:43; :: thesis: verum