let P be Subset of (TOP-REAL 2); for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds
P is_S-P_arc_joining p2,p1
let p1, p2 be Point of (TOP-REAL 2); ( P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1 )
given f being FinSequence of (TOP-REAL 2) such that A1:
f is being_S-Seq
and
A2:
P = L~ f
and
A3:
p1 = f /. 1
and
A4:
p2 = f /. (len f)
; TOPREAL4:def 1 P is_S-P_arc_joining p2,p1
take g = Rev f; TOPREAL4:def 1 ( g is being_S-Seq & P = L~ g & p2 = g /. 1 & p1 = g /. (len g) )
thus
( g is being_S-Seq & P = L~ g )
by A1, A2, Th22; ( p2 = g /. 1 & p1 = g /. (len g) )
len g = len f
by FINSEQ_5:def 3;
hence
( p2 = g /. 1 & p1 = g /. (len g) )
by A1, A3, A4, FINSEQ_5:65; verum