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

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