theorem :: SIMPLEX0:13

for X being set
for Y being Subset-Family of X st Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y holds
ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )