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