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' by A5, TOPREAL1:4;
A10: p2 in P1' by A5, TOPREAL1:4;
A11: p1 in P2 by A3, TOPREAL1:4;
A12: p2 in P2 by A3, TOPREAL1:4;
A13: p1 in P1 by A2, TOPREAL1:4;
A14: p2 in P1 by A2, TOPREAL1:4;
A15: P1 c= P by A4, XBOOLE_1:7;
A16: [#] ((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 A15, A16, XBOOLE_1:1;
A17: 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 A16, A17, XBOOLE_1:1;
A18: 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 A16, A18, XBOOLE_1:1;
A19: 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 A16, A19, XBOOLE_1:1;
A20: Q1 \/ Q2 = P \ {p1,p2} by A4, XBOOLE_1:42;
A21: Q1' \/ Q2' = P \ {p1,p2} by A7, XBOOLE_1:42;
then A22: Q1' \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, XBOOLE_1:7, XBOOLE_1:12;
A23: Q2' \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
A24: Q1 \/ (Q1' \/ Q2') = Q1' \/ Q2' by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
A25: Q2 \/ (Q1' \/ Q2') = Q1' \/ Q2' by A20, A21, 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 A26: 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 A27: 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 A28: 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 A29: Q2' is connected by A7, Th54, XBOOLE_1:7;
A30: {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 A13, A14, TARSKI:def 2; :: thesis: verum

end;

A31: {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 A11, A12, TARSKI:def 2; :: thesis: verum

end;

A32: {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, A10, TARSKI:def 2; :: thesis: verum

end;

A33: {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;

A34: Q1 \/ {p1,p2} = P1 by A30, XBOOLE_1:45;
A35: Q2 \/ {p1,p2} = P2 by A31, XBOOLE_1:45;
A36: Q1' \/ {p1,p2} = P1' by A32, XBOOLE_1:45;
A37: Q2' \/ {p1,p2} = P2' by A33, XBOOLE_1:45;

now

assume A38: ( 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 A38;

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

A40: now

assume that
A41: Q1 \ Q2' = {} and
A42: Q2' \ Q1 = {} ; :: thesis: contradiction
A43: Q1 c= Q2' by A41, XBOOLE_1:37;
Q2' c= Q1 by A42, XBOOLE_1:37;
hence contradiction by A34, A37, A39, A43, XBOOLE_0:def 10; :: thesis: verum

end;

now

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

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

consider y being Element of Q1 \ Q2';
A45: y in Q1 by A44, XBOOLE_0:def 5;
then A46: y in Q1' \/ Q2' by A20, A21, XBOOLE_0:def 3;
not y in Q2' by A44, XBOOLE_0:def 5;
then y in Q1' by A46, XBOOLE_0:def 3;
then Q1 /\ Q1' <> {} by A45, XBOOLE_0:def 4;
then A47: Q1 meets Q1' by XBOOLE_0:def 7;

now

assume Q2 meets Q1' ; :: thesis: contradiction
then (Q1 \/ Q1') \/ Q2 is connected by A26, A27, A28, A47, JORDAN1:7;
hence contradiction by A8, A13, A14, A15, A20, A22, Th60, XBOOLE_1:4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in Q2' )
assume A50: 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 A20, A21, XBOOLE_0:def 3;
hence x in Q2' by A48, A50, 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 A51: x in Q1' ; :: thesis: x in Q1
then x in Q1 \/ Q2 by A20, A21, XBOOLE_0:def 3;
then ( x in Q1 or x in Q2 ) by XBOOLE_0:def 3;
hence x in Q1 by A48, A51, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A49, Th59, XBOOLE_1:9; :: thesis: verum

end;

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

consider y being Element of Q2' \ Q1;
A53: y in Q2' by A52, XBOOLE_0:def 5;
then A54: y in Q2 \/ Q1 by A20, A21, XBOOLE_0:def 3;
not y in Q1 by A52, XBOOLE_0:def 5;
then y in Q2 by A54, XBOOLE_0:def 3;
then Q2' /\ Q2 <> {} by A53, XBOOLE_0:def 4;
then A55: Q2' meets Q2 by XBOOLE_0:def 7;

now

assume Q1' meets Q2 ; :: thesis: contradiction
then (Q2' \/ Q2) \/ Q1' is connected by A27, A28, A29, A55, JORDAN1:7;
hence contradiction by A8, A13, A14, A15, A21, A25, Th60, XBOOLE_1:4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1' or x in Q1 )
assume A58: 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 A20, A21, XBOOLE_0:def 3;
hence x in Q1 by A56, A58, 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 A59: 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 A20, A21, XBOOLE_0:def 3;
hence x in Q2' by A56, A59, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A57, Th59, XBOOLE_1:9; :: thesis: verum

end;

end;

end;

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

end;

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

A61: now

assume that
A62: Q2 \ Q1' = {} and
A63: Q1' \ Q2 = {} ; :: thesis: contradiction
A64: Q2 c= Q1' by A62, XBOOLE_1:37;
Q1' c= Q2 by A63, XBOOLE_1:37;
hence contradiction by A35, A36, A60, A64, XBOOLE_0:def 10; :: thesis: verum

end;

now

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

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

consider y being Element of Q2 \ Q1';
A66: y in Q2 by A65, XBOOLE_0:def 5;
then A67: y in Q2' \/ Q1' by A20, A21, XBOOLE_0:def 3;
not y in Q1' by A65, XBOOLE_0:def 5;
then y in Q2' by A67, XBOOLE_0:def 3;
then Q2 /\ Q2' <> {} by A66, XBOOLE_0:def 4;
then A68: Q2 meets Q2' by XBOOLE_0:def 7;

now

assume Q1 meets Q2' ; :: thesis: contradiction
then (Q2 \/ Q2') \/ Q1 is connected by A26, A27, A29, A68, JORDAN1:7;
hence contradiction by A8, A13, A14, A15, A20, A23, Th60, XBOOLE_1:4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in Q1' )
assume A71: 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 A20, A21, XBOOLE_0:def 3;
hence x in Q1' by A69, A71, 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 A72: x in Q2' ; :: thesis: x in Q2
then x in Q2 \/ Q1 by A20, A21, XBOOLE_0:def 3;
then ( x in Q2 or x in Q1 ) by XBOOLE_0:def 3;
hence x in Q2 by A69, A72, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A70, Th59, XBOOLE_1:9; :: thesis: verum

end;

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

consider y being Element of Q1' \ Q2;
A74: y in Q1' by A73, XBOOLE_0:def 5;
then A75: y in Q1 \/ Q2 by A20, A21, XBOOLE_0:def 3;
not y in Q2 by A73, XBOOLE_0:def 5;
then y in Q1 by A75, XBOOLE_0:def 3;
then Q1' /\ Q1 <> {} by A74, XBOOLE_0:def 4;
then A76: Q1' meets Q1 by XBOOLE_0:def 7;

now

assume Q2' meets Q1 ; :: thesis: contradiction
then (Q1' \/ Q1) \/ Q2' is connected by A26, A28, A29, A76, JORDAN1:7;
hence contradiction by A8, A13, A14, A15, A21, A24, Th60, XBOOLE_1:4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2' or x in Q2 )
assume A79: 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 A20, A21, XBOOLE_0:def 3;
hence x in Q2 by A77, A79, 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 A80: x in Q1 ; :: thesis: x in Q1'
then x in Q1' \/ Q2' by A20, A21, XBOOLE_0:def 3;
then ( x in Q1' or x in Q2' ) by XBOOLE_0:def 3;
hence x in Q1' by A77, A80, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P1' & P2 = P2' ) or ( P1 = P2' & P2 = P1' ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A78, 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