let f be non 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 & 1 <= 1 + 1 & 1 <= len f & 1 + 1 < len f & (1 + 1) + 1 <= len f & 1 <> 1 + 1 ) by GOBOARD7:36, XXREAL_0:2;
set i1 = 1;
set i2 = 1 + 1;
consider g1, g2 being FinSequence of (TOP-REAL 2) such that
A3: ( g1 is_a_part_of f,1,1 + 1 & g2 is_a_part_of f,1,1 + 1 & (L~ g1) /\ (L~ g2) = {(f . 1),(f . (1 + 1))} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. 1,f /. (1 + 1) & L~ g2 is_S-P_arc_joining f /. 1,f /. (1 + 1) & ( 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, Th62;
reconsider L1 = L~ g1, L2 = L~ g2 as non empty Subset of (TOP-REAL 2) by A3;
A4: L1 is_an_arc_of f /. 1,f /. (1 + 1) by A3, TOPREAL4:3;
A5: L2 is_an_arc_of f /. 1,f /. (1 + 1) by A3, TOPREAL4:3;
A6: f . 1 = f /. 1 by A2, FINSEQ_4:24;
A7: f . (1 + 1) = f /. (1 + 1) by A2, FINSEQ_4:24;
A8: f /. 1 <> f /. (1 + 1) by A2, GOBOARD7:38;
f /. 1 in (L~ g1) /\ (L~ g2) by A3, A6, TARSKI:def 2;
then f /. 1 in L~ g1 by XBOOLE_0:def 4;
then A9: f /. 1 in P by A1, A3, XBOOLE_0:def 3;
f /. (1 + 1) in (L~ g1) /\ (L~ g2) by A3, A7, TARSKI:def 2;
then f /. (1 + 1) in L~ g2 by XBOOLE_0:def 4;
then f /. (1 + 1) in P by A1, A3, XBOOLE_0:def 3;
hence P is being_simple_closed_curve by A1, A3, A4, A5, A6, A7, A8, A9, TOPREAL2:6; :: thesis: verum