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 B holds
ex D being subsequence of A st
for i being Nat holds D . i c= C . i