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 that
A1: g is_a_part_of f,i1,i2 and
A2: i1 <> i2 ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

now

per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A1, Def4;

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

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

end;

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

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

end;

end;

end;

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