let P, P1, P2, P19, P29 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 & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds
( P1 = P29 & P2 = P19 )
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 & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) implies ( P1 = P29 & P2 = P19 ) )
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: P19 is_an_arc_of p1,p2 and
A6: P29 is_an_arc_of p1,p2 and
A7: P19 \/ P29 = P ; :: thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
reconsider P = P as Simple_closed_curve by A1;
A8: p1 <> p2 by A6, Th37;
A9: p1 in P19 by A5, TOPREAL1:1;
A10: p2 in P19 by A5, TOPREAL1:1;
A11: p1 in P2 by A3, TOPREAL1:1;
A12: p2 in P2 by A3, TOPREAL1:1;
A13: p1 in P1 by A2, TOPREAL1:1;
A14: p2 in P1 by A2, TOPREAL1:1;
A15: P1 c= P by A4, XBOOLE_1:7;
A16: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;
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: P19 c= P by A7, XBOOLE_1:7;
P19 \ {p1,p2} c= P19 by XBOOLE_1:36;
then reconsider Q19 = P19 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A18, XBOOLE_1:1;
A19: P29 c= P by A7, XBOOLE_1:7;
P29 \ {p1,p2} c= P29 by XBOOLE_1:36;
then reconsider Q29 = P29 \ {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: Q19 \/ Q29 = P \ {p1,p2} by A7, XBOOLE_1:42;
then A22: Q19 \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, XBOOLE_1:7, XBOOLE_1:12;
A23: Q29 \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
A24: Q1 \/ (Q19 \/ Q29) = Q19 \/ Q29 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
A25: Q2 \/ (Q19 \/ Q29) = Q19 \/ Q29 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
[#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def 5;
then reconsider R1 = Q1 as Subset of ((TOP-REAL 2) | P1) by XBOOLE_1:36;
R1 is connected by A2, Th40;
then A26: Q1 is connected by A4, Th41, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def 5;
then reconsider R2 = Q2 as Subset of ((TOP-REAL 2) | P2) by XBOOLE_1:36;
R2 is connected by A3, Th40;
then A27: Q2 is connected by A4, Th41, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P19) = P19 by PRE_TOPC:def 5;
then reconsider R19 = Q19 as Subset of ((TOP-REAL 2) | P19) by XBOOLE_1:36;
R19 is connected by A5, Th40;
then A28: Q19 is connected by A7, Th41, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P29) = P29 by PRE_TOPC:def 5;
then reconsider R29 = Q29 as Subset of ((TOP-REAL 2) | P29) by XBOOLE_1:36;
R29 is connected by A6, Th40;
then A29: Q29 is connected by A7, Th41, XBOOLE_1:7;
A30: {p1,p2} c= P1 by A13, A14, TARSKI:def 2;
A31: {p1,p2} c= P2 by A11, A12, TARSKI:def 2;
A32: {p1,p2} c= P19 by A9, A10, TARSKI:def 2;
A33: {p1,p2} c= P29

proof

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

end;

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

now :: thesis: ( ( not P1 = P29 or not P2 = P19 ) & not ( P1 = P19 & P2 = P29 ) implies ( P1 = P29 & P2 = P19 ) )

assume A38: ( not P1 = P29 or not P2 = P19 ) ; :: thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )

now :: thesis: ( ( P1 <> P29 & ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ) or ( P2 <> P19 & ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ) )

per cases ( P1 <> P29 or P2 <> P19 ) by A38;

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

A40: now :: thesis: ( Q1 \ Q29 = {} implies not Q29 \ Q1 = {} )

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

end;

now :: thesis: ( ( Q1 \ Q29 <> {} & ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ) or ( Q29 \ Q1 <> {} & ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ) )

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

case A44: Q1 \ Q29 <> {} ; :: thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )

set y = the Element of Q1 \ Q29;
A45: the Element of Q1 \ Q29 in Q1 by A44, XBOOLE_0:def 5;
then A46: the Element of Q1 \ Q29 in Q19 \/ Q29 by A20, A21, XBOOLE_0:def 3;
not the Element of Q1 \ Q29 in Q29 by A44, XBOOLE_0:def 5;
then the Element of Q1 \ Q29 in Q19 by A46, XBOOLE_0:def 3;
then Q1 /\ Q19 <> {} by A45, XBOOLE_0:def 4;
then A47: Q1 meets Q19 ;

now :: thesis: not Q2 meets Q19

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

end;

then A48: Q2 /\ Q19 = {} ;
A49: Q2 c= Q29

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in Q29 )
assume A50: x in Q2 ; :: thesis: x in Q29
then x in Q1 \/ Q2 by XBOOLE_0:def 3;
then ( x in Q19 or x in Q29 ) by A20, A21, XBOOLE_0:def 3;
hence x in Q29 by A48, A50, XBOOLE_0:def 4; :: thesis: verum

end;

Q19 c= Q1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q19 or x in Q1 )
assume A51: x in Q19 ; :: 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 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A49, Th46, XBOOLE_1:9; :: thesis: verum

end;

case A52: Q29 \ Q1 <> {} ; :: thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )

set y = the Element of Q29 \ Q1;
A53: the Element of Q29 \ Q1 in Q29 by A52, XBOOLE_0:def 5;
then A54: the Element of Q29 \ Q1 in Q2 \/ Q1 by A20, A21, XBOOLE_0:def 3;
not the Element of Q29 \ Q1 in Q1 by A52, XBOOLE_0:def 5;
then the Element of Q29 \ Q1 in Q2 by A54, XBOOLE_0:def 3;
then Q29 /\ Q2 <> {} by A53, XBOOLE_0:def 4;
then A55: Q29 meets Q2 ;

now :: thesis: not Q19 meets Q2

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

end;

then A56: Q19 /\ Q2 = {} ;
A57: Q19 c= Q1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q19 or x in Q1 )
assume A58: x in Q19 ; :: thesis: x in Q1
then x in Q19 \/ Q29 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= Q29

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in Q29 )
assume A59: x in Q2 ; :: thesis: x in Q29
then x in Q2 \/ Q1 by XBOOLE_0:def 3;
then ( x in Q29 or x in Q19 ) by A20, A21, XBOOLE_0:def 3;
hence x in Q29 by A56, A59, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

A61: now :: thesis: ( Q2 \ Q19 = {} implies not Q19 \ Q2 = {} )

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

end;

now :: thesis: ( ( Q2 \ Q19 <> {} & ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ) or ( Q19 \ Q2 <> {} & ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ) )

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

case A65: Q2 \ Q19 <> {} ; :: thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )

set y = the Element of Q2 \ Q19;
A66: the Element of Q2 \ Q19 in Q2 by A65, XBOOLE_0:def 5;
then A67: the Element of Q2 \ Q19 in Q29 \/ Q19 by A20, A21, XBOOLE_0:def 3;
not the Element of Q2 \ Q19 in Q19 by A65, XBOOLE_0:def 5;
then the Element of Q2 \ Q19 in Q29 by A67, XBOOLE_0:def 3;
then Q2 /\ Q29 <> {} by A66, XBOOLE_0:def 4;
then A68: Q2 meets Q29 ;

now :: thesis: not Q1 meets Q29

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

end;

then A69: Q1 /\ Q29 = {} ;
A70: Q1 c= Q19

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in Q19 )
assume A71: x in Q1 ; :: thesis: x in Q19
then x in Q2 \/ Q1 by XBOOLE_0:def 3;
then ( x in Q29 or x in Q19 ) by A20, A21, XBOOLE_0:def 3;
hence x in Q19 by A69, A71, XBOOLE_0:def 4; :: thesis: verum

end;

Q29 c= Q2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q29 or x in Q2 )
assume A72: x in Q29 ; :: 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 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A70, Th46, XBOOLE_1:9; :: thesis: verum

end;

case A73: Q19 \ Q2 <> {} ; :: thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )

set y = the Element of Q19 \ Q2;
A74: the Element of Q19 \ Q2 in Q19 by A73, XBOOLE_0:def 5;
then A75: the Element of Q19 \ Q2 in Q1 \/ Q2 by A20, A21, XBOOLE_0:def 3;
not the Element of Q19 \ Q2 in Q2 by A73, XBOOLE_0:def 5;
then the Element of Q19 \ Q2 in Q1 by A75, XBOOLE_0:def 3;
then Q19 /\ Q1 <> {} by A74, XBOOLE_0:def 4;
then A76: Q19 meets Q1 ;

now :: thesis: not Q29 meets Q1

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

end;

then A77: Q29 /\ Q1 = {} ;
A78: Q29 c= Q2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q29 or x in Q2 )
assume A79: x in Q29 ; :: thesis: x in Q2
then x in Q29 \/ Q19 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= Q19

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in Q19 )
assume A80: x in Q1 ; :: thesis: x in Q19
then x in Q19 \/ Q29 by A20, A21, XBOOLE_0:def 3;
then ( x in Q19 or x in Q29 ) by XBOOLE_0:def 3;
hence x in Q19 by A77, A80, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A78, Th46, XBOOLE_1:9; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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