let P be Subset of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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) ; :: according to TOPREAL4:def 1 :: thesis: P is_S-P_arc_joining p2,p1
take g = Rev f; :: according to TOPREAL4:def 1 :: thesis: ( 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; :: thesis: ( 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; :: thesis: verum