consider C being Simple_closed_curve;
consider n being Element of NAT ;
A1: len (Upper_Seq C,n) >= 2 by TOPREAL1:def 10;
A2: 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. )
thus ( not Upper_Seq C,n is constant & Upper_Seq C,n is standard & Upper_Seq C,n is s.c.c. ) by A1, A2, JGRAPH_1:16, JORDAN8:8; :: thesis: verum