let f be S-Sequence_in_R2; :: thesis: Rev f is being_S-Seq
set g = Rev f;
thus Rev f is one-to-one ; :: according to TOPREAL1:def 10 :: thesis: ( 2 <= len (Rev f) & Rev f is unfolded & Rev f is s.n.c. & Rev f is special )
len (Rev f) = len f by FINSEQ_5:def 3;
hence len (Rev f) >= 2 by TOPREAL1:def 10; :: thesis: ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special )
thus ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special ) by Th29, Th36, Th42; :: thesis: verum