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 3 :: thesis: Rev g is_S-Seq_joining p2,p1
thus Rev g is being_S-Seq by A1, SPPOL_2:47; :: according to JORDAN3:def 3 :: thesis: ( (Rev g) . 1 = p2 & (Rev g) . (len (Rev g)) = p1 )
thus (Rev g) . 1 = p2 by A3, FINSEQ_5:65; :: thesis: (Rev g) . (len (Rev g)) = p1
dom g = dom (Rev g) by FINSEQ_5:60;
hence (Rev g) . (len (Rev g)) = (Rev g) . (len g) by FINSEQ_3:31
.= p1 by A2, FINSEQ_5:65 ;
:: thesis: verum