let g be FinSequence of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st g is_S-Seq_joining p1,p2 holds

Rev g is_S-Seq_joining p2,p1

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( g is_S-Seq_joining p1,p2 implies Rev g is_S-Seq_joining p2,p1 )

assume that

A1: g is being_S-Seq and

A2: g . 1 = p1 and

A3: g . (len g) = p2 ; :: according to JORDAN3:def 2 :: thesis: Rev g is_S-Seq_joining p2,p1

thus Rev g is being_S-Seq by A1; :: according to JORDAN3:def 2 :: thesis: ( (Rev g) . 1 = p2 & (Rev g) . (len (Rev g)) = p1 )

thus (Rev g) . 1 = p2 by A3, FINSEQ_5:62; :: thesis: (Rev g) . (len (Rev g)) = p1

dom g = dom (Rev g) by FINSEQ_5:57;

hence (Rev g) . (len (Rev g)) = (Rev g) . (len g) by FINSEQ_3:29

.= p1 by A2, FINSEQ_5:62 ;

:: thesis: verum

Rev g is_S-Seq_joining p2,p1

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( g is_S-Seq_joining p1,p2 implies Rev g is_S-Seq_joining p2,p1 )

assume that

A1: g is being_S-Seq and

A2: g . 1 = p1 and

A3: g . (len g) = p2 ; :: according to JORDAN3:def 2 :: thesis: Rev g is_S-Seq_joining p2,p1

thus Rev g is being_S-Seq by A1; :: according to JORDAN3:def 2 :: thesis: ( (Rev g) . 1 = p2 & (Rev g) . (len (Rev g)) = p1 )

thus (Rev g) . 1 = p2 by A3, FINSEQ_5:62; :: thesis: (Rev g) . (len (Rev g)) = p1

dom g = dom (Rev g) by FINSEQ_5:57;

hence (Rev g) . (len (Rev g)) = (Rev g) . (len g) by FINSEQ_3:29

.= p1 by A2, FINSEQ_5:62 ;

:: thesis: verum