theorem Th4: :: FRECHET2:4

for T being non empty 1-sorted
for S being sequence of T
for A, B being Subset of T st rng S c= A \/ B holds
ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B )