set i1 = 1;
set i2 = 1 + 1;
let f be constant standard special_circular_sequence; :: thesis: for P being non empty Subset of (TOP-REAL 2) st P = L~ f holds
P is being_simple_closed_curve
let P be non empty Subset of (TOP-REAL 2); :: thesis: ( P = L~ f implies P is being_simple_closed_curve )
assume A1: P = L~ f ; :: thesis: P is being_simple_closed_curve
A2: 1 + 1 < len f by GOBOARD7:34, XXREAL_0:2;
then A3: f /. 1 <> f /. (1 + 1) by GOBOARD7:36;
(1 + 1) + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then consider g1, g2 being FinSequence of (TOP-REAL 2) such that
g1 is_a_part_of f,1,1 + 1 and
g2 is_a_part_of f,1,1 + 1 and
A4: (L~ g1) /\ (L~ g2) = {(f . 1),(f . (1 + 1))} and
A5: (L~ g1) \/ (L~ g2) = L~ f and
A6: L~ g1 is_S-P_arc_joining f /. 1,f /. (1 + 1) and
A7: L~ g2 is_S-P_arc_joining f /. 1,f /. (1 + 1) and
for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,1,1 + 1 or g = g1 or g = g2 ) by A2, Th50;
reconsider L1 = L~ g1, L2 = L~ g2 as non empty Subset of (TOP-REAL 2) by A4;
A8: L2 is_an_arc_of f /. 1,f /. (1 + 1) by A7, TOPREAL4:2;
1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A9: f . 1 = f /. 1 by FINSEQ_4:15;
then f /. 1 in (L~ g1) /\ (L~ g2) by A4, TARSKI:def 2;
then f /. 1 in L~ g1 by XBOOLE_0:def 4;
then A10: f /. 1 in P by A1, A5, XBOOLE_0:def 3;
A11: f . (1 + 1) = f /. (1 + 1) by A2, FINSEQ_4:15;
then f /. (1 + 1) in (L~ g1) /\ (L~ g2) by A4, TARSKI:def 2;
then f /. (1 + 1) in L~ g2 by XBOOLE_0:def 4;
then A12: f /. (1 + 1) in P by A1, A5, XBOOLE_0:def 3;
L1 is_an_arc_of f /. 1,f /. (1 + 1) by A6, TOPREAL4:2;
hence P is being_simple_closed_curve by A1, A4, A5, A8, A9, A11, A3, A10, A12, TOPREAL2:6; :: thesis: verum