theorem Th32: :: KURATO_2:32

for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds A . i c= B . i ) & C is subsequence of A holds
ex D being subsequence of B st
for i being Nat holds C . i c= D . i