theorem Th2: :: MSAFREE5:11

for I, J being FinSequence-membered set
for p, q being FinSequence st len p = len q & p <> q holds
p ^^ I misses q ^^ J