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