consider f being being_S-Seq FinSequence of (TOP-REAL 2);
( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) ;
hence ex b₁ being FinSequence of (TOP-REAL 2) st
( b₁ is one-to-one & b₁ is unfolded & b₁ is s.n.c. & b₁ is special & not b₁ is trivial ) ; :: thesis: verum