theorem Th15: :: SIMPLEX1:15

for V being RealLinearSpace
for K being with_empty_element SimplicialComplex of V st |.K.| c= [#] K holds
for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ) holds
subdivision (B,K) is SubdivisionStr of K