theorem Th12: :: YELLOW15:15

for X being set
for p being FinSequence of bool X holds { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } is Subset-Family of X