consider n being Element of NAT ;
consider C being Simple_closed_curve;
A1: Upper_Seq C,n is_sequence_on Gauge C,n by JORDAN1G:4;
take Upper_Seq C,n ; :: thesis: ( not Upper_Seq C,n is constant & Upper_Seq C,n is standard & Upper_Seq C,n is s.c.c. )
len (Upper_Seq C,n) >= 2 by TOPREAL1:def 10;
hence ( not Upper_Seq C,n is constant & Upper_Seq C,n is standard & Upper_Seq C,n is s.c.c. ) by A1, JGRAPH_1:16, JORDAN8:8; :: thesis: verum