theorem Th15: :: PRE_POLY:16

for V, C being set holds PFuncs (V,C) c= bool [:V,C:]