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

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;

( 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

A34:
Q1 \/ {p1,p2} = P1
by A30, XBOOLE_1:45;
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;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

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 ) )

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

end;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 ) ) ) )end;

hence
( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
; :: thesis: verumper cases
( P1 <> P29 or P2 <> P19 )
by A38;

end;

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

end;

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;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

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 ) ) ) )end;

hence
( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
; :: thesis: verumper cases
( Q1 \ Q29 <> {} or Q29 \ Q1 <> {} )
by A40;

end;

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 ;

A49: Q2 c= Q29

end;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

then A48:
Q2 /\ 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 (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

A49: Q2 c= Q29

proof

Q19 c= Q1
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;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

proof

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
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;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

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 ;

A57: Q19 c= Q1

end;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

then A56:
Q19 /\ 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 (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

A57: Q19 c= Q1

proof

Q2 c= Q29
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;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

proof

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
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;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

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

end;

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;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

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 ) ) ) )end;

hence
( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
; :: thesis: verumper cases
( Q2 \ Q19 <> {} or Q19 \ Q2 <> {} )
by A61;

end;

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 ;

A70: Q1 c= Q19

end;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

then A69:
Q1 /\ 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 (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

A70: Q1 c= Q19

proof

Q29 c= Q2
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;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

proof

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
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;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

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 ;

A78: Q29 c= Q2

end;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

then A77:
Q29 /\ 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 (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

A78: Q29 c= Q2

proof

Q1 c= Q19
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;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

proof

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
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;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