let A be Subset of (Complex_of F); :: 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 subset-closed_closure_of F ;
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