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

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