theorem Th17: :: MEASURE1:17

for X being set
for A, B, C being Subset of X ex F being sequence of (bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )