theorem Th22: :: SIMPLEX2:22

for n being Nat
for A being non empty affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A
for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty