let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part<_of f,i1,i2 & i1 <> i2 implies L~ g is_S-P_arc_joining f /. i1,f /. i2 )
assume A1: ( g is_a_part<_of f,i1,i2 & i1 <> i2 ) ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

now

per cases ( i1 > i2 or i1 <= i2 ) ;

case i1 > i2 ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

then A2: L~ (Rev g) is_S-P_arc_joining f /. i2,f /. i1 by A1, Th42, Th56;
reconsider p2 = f /. i2, p1 = f /. i1 as Point of (TOP-REAL 2) ;
reconsider P = L~ g as Subset of (TOP-REAL 2) ;
P is_S-P_arc_joining p2,p1 by A2, SPPOL_2:22;
hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by SPPOL_2:53; :: thesis: verum

end;

case i1 <= i2 ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

then i1 < i2 by A1, XXREAL_0:1;
then A3: L~ (Rev g) is_S-P_arc_joining f /. i2,f /. i1 by A1, Lm1, Th42;
reconsider p2 = f /. i2, p1 = f /. i1 as Point of (TOP-REAL 2) ;
reconsider P = L~ g as Subset of (TOP-REAL 2) ;
P is_S-P_arc_joining p2,p1 by A3, SPPOL_2:22;
hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by SPPOL_2:53; :: thesis: verum

end;

end;

end;

hence L~ g is_S-P_arc_joining f /. i1,f /. i2 ; :: thesis: verum