let P, P1, P2, P1', P2' be Subset of the carrier of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1' is_an_arc_of p1,p2 & P2' is_an_arc_of p1,p2 & P1' \/ P2' = P & not ( P1 = P1' & P2 = P2' ) holds
( P1 = P2' & P2 = P1' )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1' is_an_arc_of p1,p2 & P2' is_an_arc_of p1,p2 & P1' \/ P2' = P & not ( P1 = P1' & P2 = P2' ) implies ( P1 = P2' & P2 = P1' ) )
assume that
A1: P is being_simple_closed_curve and
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P1 \/ P2 = P and
A5: P1' is_an_arc_of p1,p2 and
A6: P2' is_an_arc_of p1,p2 and
A7: P1' \/ P2' = P ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )
reconsider P = P as Simple_closed_curve by A1;
A8: p1 <> p2 by A6, Th49;
A9: ( p1 in P1' & p2 in P1' ) by A5, TOPREAL1:4;
A10: ( p1 in P2 & p2 in P2 ) by A3, TOPREAL1:4;
A11: ( p1 in P1 & p2 in P1 ) by A2, TOPREAL1:4;
A12: P1 c= P by A4, XBOOLE_1:7;
A13: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 10;
P1 \ {p1,p2} c= P1 by XBOOLE_1:36;
then reconsider Q1 = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A12, A13, XBOOLE_1:1;
A14: P2 c= P by A4, XBOOLE_1:7;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider Q2 = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A13, A14, XBOOLE_1:1;
A15: P1' c= P by A7, XBOOLE_1:7;
P1' \ {p1,p2} c= P1' by XBOOLE_1:36;
then reconsider Q1' = P1' \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A13, A15, XBOOLE_1:1;
A16: P2' c= P by A7, XBOOLE_1:7;
P2' \ {p1,p2} c= P2' by XBOOLE_1:36;
then reconsider Q2' = P2' \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A13, A16, XBOOLE_1:1;
A17: Q1 \/ Q2 = P \ {p1,p2} by A4, XBOOLE_1:42;
A18: Q1' \/ Q2' = P \ {p1,p2} by A7, XBOOLE_1:42;
then A19: Q1' \/ (Q1 \/ Q2) = Q1 \/ Q2 by A17, XBOOLE_1:7, XBOOLE_1:12;
A20: Q2' \/ (Q1 \/ Q2) = Q1 \/ Q2 by A17, A18, XBOOLE_1:7, XBOOLE_1:12;
A21: Q1 \/ (Q1' \/ Q2') = Q1' \/ Q2' by A17, A18, XBOOLE_1:7, XBOOLE_1:12;
A22: Q2 \/ (Q1' \/ Q2') = Q1' \/ Q2' by A17, A18, XBOOLE_1:7, XBOOLE_1:12;
[#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def 10;
then reconsider R1 = Q1 as Subset of ((TOP-REAL 2) | P1) by XBOOLE_1:36;
R1 is connected by A2, Th53;
then A23: Q1 is connected by A4, Th54, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def 10;
then reconsider R2 = Q2 as Subset of ((TOP-REAL 2) | P2) by XBOOLE_1:36;
R2 is connected by A3, Th53;
then A24: Q2 is connected by A4, Th54, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P1') = P1' by PRE_TOPC:def 10;
then reconsider R1' = Q1' as Subset of ((TOP-REAL 2) | P1') by XBOOLE_1:36;
R1' is connected by A5, Th53;
then A25: Q1' is connected by A7, Th54, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P2') = P2' by PRE_TOPC:def 10;
then reconsider R2' = Q2' as Subset of ((TOP-REAL 2) | P2') by XBOOLE_1:36;
R2' is connected by A6, Th53;
then A26: Q2' is connected by A7, Th54, XBOOLE_1:7;
A27: {p1,p2} c= P1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {p1,p2} or x in P1 )
assume x in {p1,p2} ; :: thesis: x in P1
hence x in P1 by A11, TARSKI:def 2; :: thesis: verum

end;

A28: {p1,p2} c= P2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {p1,p2} or x in P2 )
assume x in {p1,p2} ; :: thesis: x in P2
hence x in P2 by A10, TARSKI:def 2; :: thesis: verum

end;

A29: {p1,p2} c= P1'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {p1,p2} or x in P1' )
assume x in {p1,p2} ; :: thesis: x in P1'
hence x in P1' by A9, TARSKI:def 2; :: thesis: verum

end;

A30: {p1,p2} c= P2'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {p1,p2} or x in P2' )
assume x in {p1,p2} ; :: thesis: x in P2'
then ( x = p1 or x = p2 ) by TARSKI:def 2;
hence x in P2' by A6, TOPREAL1:4; :: thesis: verum

end;

A31: Q1 \/ {p1,p2} = P1 by A27, XBOOLE_1:45;
A32: Q2 \/ {p1,p2} = P2 by A28, XBOOLE_1:45;
A33: Q1' \/ {p1,p2} = P1' by A29, XBOOLE_1:45;
A34: Q2' \/ {p1,p2} = P2' by A30, XBOOLE_1:45;

now

assume A35: ( not P1 = P2' or not P2 = P1' ) ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

now

per cases ( P1 <> P2' or P2 <> P1' ) by A35;

case A36: P1 <> P2' ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

A37: now

assume A38: ( Q1 \ Q2' = {} & Q2' \ Q1 = {} ) ; :: thesis: contradiction
then A39: Q1 c= Q2' by XBOOLE_1:37;
Q2' c= Q1 by A38, XBOOLE_1:37;
hence contradiction by A31, A34, A36, A39, XBOOLE_0:def 10; :: thesis: verum

end;

now

per cases ( Q1 \ Q2' <> {} or Q2' \ Q1 <> {} ) by A37;

case A40: Q1 \ Q2' <> {} ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

consider y being Element of Q1 \ Q2';
A41: y in Q1 by A40, XBOOLE_0:def 5;
then A42: y in Q1' \/ Q2' by A17, A18, XBOOLE_0:def 3;
not y in Q2' by A40, XBOOLE_0:def 5;
then y in Q1' by A42, XBOOLE_0:def 3;
then Q1 /\ Q1' <> {} by A41, XBOOLE_0:def 4;
then A43: Q1 meets Q1' by XBOOLE_0:def 7;

now

assume Q2 meets Q1' ; :: thesis: contradiction
then (Q1 \/ Q1') \/ Q2 is connected by A23, A24, A25, A43, JORDAN1:7;
hence contradiction by A8, A11, A12, A17, A19, Th60, XBOOLE_1:4; :: thesis: verum

end;

then A44: Q2 /\ Q1' = {} by XBOOLE_0:def 7;
A45: Q2 c= Q2'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in Q2' )
assume A46: x in Q2 ; :: thesis: x in Q2'
then x in Q1 \/ Q2 by XBOOLE_0:def 3;
then ( x in Q1' or x in Q2' ) by A17, A18, XBOOLE_0:def 3;
hence x in Q2' by A44, A46, XBOOLE_0:def 4; :: thesis: verum

end;

Q1' c= Q1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1' or x in Q1 )
assume A47: x in Q1' ; :: thesis: x in Q1
then x in Q1 \/ Q2 by A17, A18, XBOOLE_0:def 3;
then ( x in Q1 or x in Q2 ) by XBOOLE_0:def 3;
hence x in Q1 by A44, A47, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A31, A32, A33, A34, A45, Th59, XBOOLE_1:9; :: thesis: verum

end;

case A48: Q2' \ Q1 <> {} ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

consider y being Element of Q2' \ Q1;
A49: y in Q2' by A48, XBOOLE_0:def 5;
then A50: y in Q2 \/ Q1 by A17, A18, XBOOLE_0:def 3;
not y in Q1 by A48, XBOOLE_0:def 5;
then y in Q2 by A50, XBOOLE_0:def 3;
then Q2' /\ Q2 <> {} by A49, XBOOLE_0:def 4;
then A51: Q2' meets Q2 by XBOOLE_0:def 7;

now

assume Q1' meets Q2 ; :: thesis: contradiction
then (Q2' \/ Q2) \/ Q1' is connected by A24, A25, A26, A51, JORDAN1:7;
hence contradiction by A8, A11, A12, A18, A22, Th60, XBOOLE_1:4; :: thesis: verum

end;

then A52: Q1' /\ Q2 = {} by XBOOLE_0:def 7;
A53: Q1' c= Q1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1' or x in Q1 )
assume A54: x in Q1' ; :: thesis: x in Q1
then x in Q1' \/ Q2' by XBOOLE_0:def 3;
then ( x in Q1 or x in Q2 ) by A17, A18, XBOOLE_0:def 3;
hence x in Q1 by A52, A54, XBOOLE_0:def 4; :: thesis: verum

end;

Q2 c= Q2'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in Q2' )
assume A55: x in Q2 ; :: thesis: x in Q2'
then x in Q2 \/ Q1 by XBOOLE_0:def 3;
then ( x in Q2' or x in Q1' ) by A17, A18, XBOOLE_0:def 3;
hence x in Q2' by A52, A55, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A31, A32, A33, A34, A53, Th59, XBOOLE_1:9; :: thesis: verum

end;

end;

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) ; :: thesis: verum

end;

case A56: P2 <> P1' ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

A57: now

assume A58: ( Q2 \ Q1' = {} & Q1' \ Q2 = {} ) ; :: thesis: contradiction
then A59: Q2 c= Q1' by XBOOLE_1:37;
Q1' c= Q2 by A58, XBOOLE_1:37;
hence contradiction by A32, A33, A56, A59, XBOOLE_0:def 10; :: thesis: verum

end;

now

per cases ( Q2 \ Q1' <> {} or Q1' \ Q2 <> {} ) by A57;

case A60: Q2 \ Q1' <> {} ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

consider y being Element of Q2 \ Q1';
A61: y in Q2 by A60, XBOOLE_0:def 5;
then A62: y in Q2' \/ Q1' by A17, A18, XBOOLE_0:def 3;
not y in Q1' by A60, XBOOLE_0:def 5;
then y in Q2' by A62, XBOOLE_0:def 3;
then Q2 /\ Q2' <> {} by A61, XBOOLE_0:def 4;
then A63: Q2 meets Q2' by XBOOLE_0:def 7;

now

assume Q1 meets Q2' ; :: thesis: contradiction
then (Q2 \/ Q2') \/ Q1 is connected by A23, A24, A26, A63, JORDAN1:7;
hence contradiction by A8, A11, A12, A17, A20, Th60, XBOOLE_1:4; :: thesis: verum

end;

then A64: Q1 /\ Q2' = {} by XBOOLE_0:def 7;
A65: Q1 c= Q1'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in Q1' )
assume A66: x in Q1 ; :: thesis: x in Q1'
then x in Q2 \/ Q1 by XBOOLE_0:def 3;
then ( x in Q2' or x in Q1' ) by A17, A18, XBOOLE_0:def 3;
hence x in Q1' by A64, A66, XBOOLE_0:def 4; :: thesis: verum

end;

Q2' c= Q2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2' or x in Q2 )
assume A67: x in Q2' ; :: thesis: x in Q2
then x in Q2 \/ Q1 by A17, A18, XBOOLE_0:def 3;
then ( x in Q2 or x in Q1 ) by XBOOLE_0:def 3;
hence x in Q2 by A64, A67, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A31, A32, A33, A34, A65, Th59, XBOOLE_1:9; :: thesis: verum

end;

case A68: Q1' \ Q2 <> {} ; :: thesis: ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) )

consider y being Element of Q1' \ Q2;
A69: y in Q1' by A68, XBOOLE_0:def 5;
then A70: y in Q1 \/ Q2 by A17, A18, XBOOLE_0:def 3;
not y in Q2 by A68, XBOOLE_0:def 5;
then y in Q1 by A70, XBOOLE_0:def 3;
then Q1' /\ Q1 <> {} by A69, XBOOLE_0:def 4;
then A71: Q1' meets Q1 by XBOOLE_0:def 7;

now

assume Q2' meets Q1 ; :: thesis: contradiction
then (Q1' \/ Q1) \/ Q2' is connected by A23, A25, A26, A71, JORDAN1:7;
hence contradiction by A8, A11, A12, A18, A21, Th60, XBOOLE_1:4; :: thesis: verum

end;

then A72: Q2' /\ Q1 = {} by XBOOLE_0:def 7;
A73: Q2' c= Q2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2' or x in Q2 )
assume A74: x in Q2' ; :: thesis: x in Q2
then x in Q2' \/ Q1' by XBOOLE_0:def 3;
then ( x in Q2 or x in Q1 ) by A17, A18, XBOOLE_0:def 3;
hence x in Q2 by A72, A74, XBOOLE_0:def 4; :: thesis: verum

end;

Q1 c= Q1'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in Q1' )
assume A75: x in Q1 ; :: thesis: x in Q1'
then x in Q1' \/ Q2' by A17, A18, XBOOLE_0:def 3;
then ( x in Q1' or x in Q2' ) by XBOOLE_0:def 3;
hence x in Q1' by A72, A75, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A31, A32, A33, A34, A73, Th59, XBOOLE_1:9; :: thesis: verum

end;

end;

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) ; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) ; :: thesis: verum