theorem Th12: :: SIMPLEX0:12

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