let f be V26() standard special_circular_sequence; for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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); for i1, i2 being 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 Nat; ( g is_a_part<_of f,i1,i2 & i1 <> i2 implies L~ g is_S-P_arc_joining f /. i1,f /. i2 )
assume that
A1:
g is_a_part<_of f,i1,i2
and
A2:
i1 <> i2
; L~ g is_S-P_arc_joining f /. i1,f /. i2
hence
L~ g is_S-P_arc_joining f /. i1,f /. i2
; verum