theorem Th12: :: SIMPLEX2:12

for n being Nat
for X being set
for A being affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }