let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) )
assume A1: f is weakly-one-to-one ; :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) = Rev (B_Cut (f,q,p))
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f implies B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) )
assume that
A2: p in L~ f and
A3: q in L~ f ; :: thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p))

per cases ( p = q or ( p <> q & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) or ( p <> q & not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ;

suppose A4: p = q ; :: thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p))

then B_Cut (f,p,q) = <*p*> by A1, A2, Th15;
hence B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A4, FINSEQ_5:60; :: thesis: verum

end;

suppose that A5: p <> q and
A6: ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; :: thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p))

( not Index (q,f) = Index (p,f) or not LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) ) by A5, A6, JORDAN3:27;
then A7: Rev (B_Cut (f,q,p)) = Rev (Rev (R_Cut ((L_Cut (f,p)),q))) by A6, JORDAN3:def 7;
B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by A2, A3, A6, JORDAN3:def 7;
hence B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A7; :: thesis: verum

end;

suppose that p <> q and
A8: ( not Index (p,f) < Index (q,f) & not ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; :: thesis: B_Cut (f,p,q) = Rev (B_Cut (f,q,p))

A9: ( Index (q,f) < Index (p,f) or ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) by A8, XXREAL_0:1;

A10: now :: thesis: ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) implies LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) )

assume that
A11: Index (p,f) = Index (q,f) and
A12: not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; :: thesis: LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1)
A13: 1 <= Index (p,f) by A2, JORDAN3:8;
A14: Index (p,f) < len f by A2, JORDAN3:8;
then A15: (Index (p,f)) + 1 <= len f by NAT_1:13;
then A16: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A13, TOPREAL1:def 3;
then A17: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN3:9;
1 <= (Index (p,f)) + 1 by NAT_1:11;
then A18: (Index (p,f)) + 1 in dom f by A15, FINSEQ_3:25;
f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A1, A13, A14;
then A19: f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A18, PARTFUN1:def 6;
Index (p,f) in dom f by A13, A14, FINSEQ_3:25;
then A20: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A19, PARTFUN1:def 6;
q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A11, A16, JORDAN3:9;
then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A12, A17, A20, JORDAN3:28;
hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A11, JORDAN3:def 6; :: thesis: verum

end;

B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A8, JORDAN3:def 7;
hence B_Cut (f,p,q) = Rev (B_Cut (f,q,p)) by A2, A3, A9, A10, JORDAN3:def 7; :: thesis: verum

end;

end;