let P, P1, P2, P19, P29 be Subset of the carrier of (); :: thesis: for p1, p2 being Point of () 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 (); :: 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 ;
A9: p1 in P19 by ;
A10: p2 in P19 by ;
A11: p1 in P2 by ;
A12: p2 in P2 by ;
A13: p1 in P1 by ;
A14: p2 in P1 by ;
A15: P1 c= P by ;
A16: [#] (() | 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 (() | P) by ;
A17: P2 c= P by ;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider Q2 = P2 \ {p1,p2} as Subset of (() | P) by ;
A18: P19 c= P by ;
P19 \ {p1,p2} c= P19 by XBOOLE_1:36;
then reconsider Q19 = P19 \ {p1,p2} as Subset of (() | P) by ;
A19: P29 c= P by ;
P29 \ {p1,p2} c= P29 by XBOOLE_1:36;
then reconsider Q29 = P29 \ {p1,p2} as Subset of (() | P) by ;
A20: Q1 \/ Q2 = P \ {p1,p2} by ;
A21: Q19 \/ Q29 = P \ {p1,p2} by ;
then A22: Q19 \/ (Q1 \/ Q2) = Q1 \/ Q2 by ;
A23: Q29 \/ (Q1 \/ Q2) = Q1 \/ Q2 by ;
A24: Q1 \/ (Q19 \/ Q29) = Q19 \/ Q29 by ;
A25: Q2 \/ (Q19 \/ Q29) = Q19 \/ Q29 by ;
[#] (() | P1) = P1 by PRE_TOPC:def 5;
then reconsider R1 = Q1 as Subset of (() | P1) by XBOOLE_1:36;
R1 is connected by ;
then A26: Q1 is connected by ;
[#] (() | P2) = P2 by PRE_TOPC:def 5;
then reconsider R2 = Q2 as Subset of (() | P2) by XBOOLE_1:36;
R2 is connected by ;
then A27: Q2 is connected by ;
[#] (() | P19) = P19 by PRE_TOPC:def 5;
then reconsider R19 = Q19 as Subset of (() | P19) by XBOOLE_1:36;
R19 is connected by ;
then A28: Q19 is connected by ;
[#] (() | P29) = P29 by PRE_TOPC:def 5;
then reconsider R29 = Q29 as Subset of (() | P29) by XBOOLE_1:36;
R29 is connected by ;
then A29: Q29 is connected by ;
A30: {p1,p2} c= P1 by ;
A31: {p1,p2} c= P2 by ;
A32: {p1,p2} c= P19 by ;
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 ; :: thesis: verum
end;
A34: Q1 \/ {p1,p2} = P1 by ;
A35: Q2 \/ {p1,p2} = P2 by ;
A36: Q19 \/ {p1,p2} = P19 by ;
A37: Q29 \/ {p1,p2} = P29 by ;
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 ;
Q29 c= Q1 by ;
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 ;
then A46: the Element of Q1 \ Q29 in Q19 \/ Q29 by ;
not the Element of Q1 \ Q29 in Q29 by ;
then the Element of Q1 \ Q29 in Q19 by ;
then Q1 /\ Q19 <> {} by ;
then A47: Q1 meets Q19 ;
now :: thesis: not Q2 meets Q19
assume Q2 meets Q19 ; :: thesis: contradiction
then (Q1 \/ Q19) \/ Q2 is connected by ;
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 ;
hence x in Q29 by ; :: 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 ;
then ( x in Q1 or x in Q2 ) by XBOOLE_0:def 3;
hence x in Q1 by ; :: 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 ;
then A54: the Element of Q29 \ Q1 in Q2 \/ Q1 by ;
not the Element of Q29 \ Q1 in Q1 by ;
then the Element of Q29 \ Q1 in Q2 by ;
then Q29 /\ Q2 <> {} by ;
then A55: Q29 meets Q2 ;
now :: thesis: not Q19 meets Q2end;
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 ;
hence x in Q1 by ; :: 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 ;
hence x in Q29 by ; :: 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 ;
Q19 c= Q2 by ;
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 ;
then A67: the Element of Q2 \ Q19 in Q29 \/ Q19 by ;
not the Element of Q2 \ Q19 in Q19 by ;
then the Element of Q2 \ Q19 in Q29 by ;
then Q2 /\ Q29 <> {} by ;
then A68: Q2 meets Q29 ;
now :: thesis: not Q1 meets Q29
assume Q1 meets Q29 ; :: thesis: contradiction
then (Q2 \/ Q29) \/ Q1 is connected by ;
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 ;
hence x in Q19 by ; :: 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 ;
then ( x in Q2 or x in Q1 ) by XBOOLE_0:def 3;
hence x in Q2 by ; :: 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 ;
then A75: the Element of Q19 \ Q2 in Q1 \/ Q2 by ;
not the Element of Q19 \ Q2 in Q2 by ;
then the Element of Q19 \ Q2 in Q1 by ;
then Q19 /\ Q1 <> {} by ;
then A76: Q19 meets Q1 ;
now :: thesis: not Q29 meets Q1end;
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 ;
hence x in Q2 by ; :: 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 ;
then ( x in Q19 or x in Q29 ) by XBOOLE_0:def 3;
hence x in Q19 by ; :: 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