theorem Th10: :: REARRAN1:10

for n being Nat
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )