let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial implies f is being_S-Seq )
assume A5: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special ) ; :: thesis: ( f is trivial or f is being_S-Seq )
assume not f is trivial ; :: thesis: f is being_S-Seq
then len f >= 2 by NAT_D:60;
hence f is being_S-Seq by A5, TOPREAL1:def 8; :: thesis: verum