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