theorem Th29: :: POLNOT_1:29

for X being set
for B being disjoint_valued FinSequence of bool X
for a, b, c being object st a in B . b & a in B . c holds
( b = c & b in dom B )