let s1, t1, s2, t2 be Real; :: thesis: for P, P1 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds
Cl P1 = P \/ P1
let P, P1 be Subset of (TOP-REAL 2); :: thesis: ( s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } implies Cl P1 = P \/ P1 )
assume that
A1: s1 < s2 and
A2: t1 < t2 and
A3: P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } and
A4: P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } ; :: thesis: Cl P1 = P \/ P1
reconsider P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } as Subset of (TOP-REAL 2) by Th24;
A5: P1 c= Cl P1 by PRE_TOPC:18;
reconsider PP = P ` as Subset of (TOP-REAL 2) ;
A6: PP = P1 \/ P2 by A1, A2, A3, A4, Th30;
P1 misses P2 by A1, A2, A3, A4, Th30;
then A7: P1 c= P2 ` by SUBSET_1:23;
P = (P1 \/ P2) ` by A6;
then A8: P = (([#] (TOP-REAL 2)) \ P1) /\ (([#] (TOP-REAL 2)) \ P2) by XBOOLE_1:53;
[#] (TOP-REAL 2) = P \/ (P1 \/ P2) by A6, PRE_TOPC:2;
then A9: [#] (TOP-REAL 2) = (P \/ P1) \/ P2 by XBOOLE_1:4;
now :: thesis: for x being object st x in P2 ` holds
x in P \/ P1
let x be object ; :: thesis: ( x in P2 ` implies x in P \/ P1 )
assume A10: x in P2 ` ; :: thesis: x in P \/ P1
then not x in P2 by XBOOLE_0:def 5;
hence x in P \/ P1 by A9, A10, XBOOLE_0:def 3; :: thesis: verum
end;
then A11: P2 ` c= P \/ P1 ;
now :: thesis: for x being object st x in P \/ P1 holds
x in P2 `
let x be object ; :: thesis: ( x in P \/ P1 implies x in P2 ` )
assume x in P \/ P1 ; :: thesis: x in P2 `
then ( x in P or x in P1 ) by XBOOLE_0:def 3;
hence x in P2 ` by A7, A8, XBOOLE_0:def 4; :: thesis: verum
end;
then P \/ P1 c= P2 ` ;
then A12: P2 ` = P \/ P1 by A11;
A13: P2 is open by Th28;
([#] (TOP-REAL 2)) \ (P2 `) = (P2 `) `
.= P2 ;
then A14: P \/ P1 is closed by A12, A13, PRE_TOPC:def 3;
A15: P1 c= P \/ P1 by XBOOLE_1:7;
thus Cl P1 c= P \/ P1 by A14, A15, PRE_TOPC:15; :: according to XBOOLE_0:def 10 :: thesis: P \/ P1 c= Cl P1
P c= Cl P1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in Cl P1 )
assume x in P ; :: thesis: x in Cl P1
then consider p being Point of (TOP-REAL 2) such that
A16: p = x and
A17: ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) by A3;
reconsider q = p as Point of (Euclid 2) by EUCLID:22;
now :: thesis: x in Cl P1
per cases ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) by A17;
suppose A18: ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) ; :: thesis: x in Cl P1
now :: thesis: p in Cl P1
per cases ( ( p `1 = s1 & p `2 < t2 & p `2 > t1 ) or ( p `1 = s1 & p `2 = t1 ) or ( p `1 = s1 & p `2 = t2 ) ) by A18, XXREAL_0:1;
suppose A19: ( p `1 = s1 & p `2 < t2 & p `2 > t1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A20: Q is open and
A21: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A20, Lm9, PRE_TOPC:30;
then consider r being Real such that
A22: r > 0 and
A23: Ball (q,r) c= Q by A21, TOPMETR:15;
reconsider r = r as Real ;
A24: r / 2 > 0 by A22, XREAL_1:215;
A25: r / 2 < r by A22, XREAL_1:216;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A26: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= r / 2 by XXREAL_0:17;
A27: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
then A28: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A27, XXREAL_0:2;
A29: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < r by A25, A26, XXREAL_0:2;
A30: s2 - s1 > 0 by A1, XREAL_1:50;
A31: t2 - t1 > 0 by A2, XREAL_1:50;
A32: (s2 - s1) / 2 > 0 by A30, XREAL_1:215;
(t2 - t1) / 2 > 0 by A31, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A32, XXREAL_0:15;
then A33: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A24, XXREAL_0:15;
set pa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]|;
A34: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1 = (p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A35: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2 = p `2 by EUCLID:52;
(s2 - s1) / 2 < s2 - s1 by A30, XREAL_1:216;
then A36: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < s2 - (p `1) by A19, A28, XXREAL_0:2;
A37: s1 < |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1 by A19, A33, A34, XREAL_1:29;
|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1 < s2 by A34, A36, XREAL_1:20;
then A38: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| in P1 by A4, A19, A35, A37;
reconsider qa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| as Point of (Euclid 2) by EUCLID:22;
A39: 0 <= ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2 by XREAL_1:63;
then A40: 0 + 0 <= (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2) by A39, XREAL_1:7;
((|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1) - (p `1)) ^2 = ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2 ;
then (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2) < r ^2 by A29, A33, A34, A35, SQUARE_1:16;
then (sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2))) ^2 < r ^2 by A40, SQUARE_1:def 2;
then A41: sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2)) < r by A22, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A41, TOPREAL3:7;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A23, A38, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A42: ( p `1 = s1 & p `2 = t1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A43: Q is open and
A44: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A43, Lm9, PRE_TOPC:30;
then consider r being Real such that
A45: r > 0 and
A46: Ball (q,r) c= Q by A44, TOPMETR:15;
reconsider r = r as Real ;
A47: r / 2 > 0 by A45, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A48: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A49: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A50: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A51: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A48, A49, XXREAL_0:2;
A52: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A48, A50, XXREAL_0:2;
A53: s2 - s1 > 0 by A1, XREAL_1:50;
A54: t2 - t1 > 0 by A2, XREAL_1:50;
A55: (s2 - s1) / 2 > 0 by A53, XREAL_1:215;
(t2 - t1) / 2 > 0 by A54, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A55, XXREAL_0:15;
then A56: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A47, XXREAL_0:15;
set pa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A57: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A58: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A59: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A42, A56, A57, XREAL_1:29;
A60: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A42, A56, A58, XREAL_1:29;
(s2 - s1) / 2 < s2 - s1 by A53, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < s2 - (p `1) by A42, A51, XXREAL_0:2;
then A61: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A57, XREAL_1:20;
(t2 - t1) / 2 < t2 - t1 by A54, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < t2 - (p `2) by A42, A52, XXREAL_0:2;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A58, XREAL_1:20;
then A62: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A59, A60, A61;
reconsider qa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A63: 0 <= ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A64: 0 + 0 <= (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A63, XREAL_1:7;
((|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1) - (p `1)) ^2 = ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 ;
then ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 <= (r / 2) ^2 by A56, A57, SQUARE_1:15, XXREAL_0:17;
then A65: (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A57, A58, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A45, A47, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A65, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A64, SQUARE_1:def 2;
then A66: sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A45, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A66, TOPREAL3:7;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A46, A62, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A67: ( p `1 = s1 & p `2 = t2 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A68: Q is open and
A69: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A68, Lm9, PRE_TOPC:30;
then consider r being Real such that
A70: r > 0 and
A71: Ball (q,r) c= Q by A69, TOPMETR:15;
reconsider r = r as Real ;
A72: r / 2 > 0 by A70, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A73: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A74: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A75: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A76: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A73, A74, XXREAL_0:2;
A77: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A73, A75, XXREAL_0:2;
A78: s2 - s1 > 0 by A1, XREAL_1:50;
A79: t2 - t1 > 0 by A2, XREAL_1:50;
A80: (s2 - s1) / 2 > 0 by A78, XREAL_1:215;
(t2 - t1) / 2 > 0 by A79, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A80, XXREAL_0:15;
then A81: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A72, XXREAL_0:15;
set pa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A82: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A83: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A84: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A67, A81, A82, XREAL_1:29;
A85: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A67, A81, A83, XREAL_1:44;
(s2 - s1) / 2 < s2 - s1 by A78, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < s2 - (p `1) by A67, A76, XXREAL_0:2;
then A86: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A82, XREAL_1:20;
(t2 - t1) / 2 < t2 - t1 by A79, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `2) - t1 by A67, A77, XXREAL_0:2;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A83, XREAL_1:12;
then A87: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A84, A85, A86;
reconsider qa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A88: 0 <= ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A89: 0 + 0 <= (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A88, XREAL_1:7;
(min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) ^2 <= (r / 2) ^2 by A81, SQUARE_1:15, XXREAL_0:17;
then A90: (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A82, A83, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A70, A72, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A90, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A89, SQUARE_1:def 2;
then A91: sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A70, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A91, TOPREAL3:7;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A71, A87, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
end;
end;
hence x in Cl P1 by A16; :: thesis: verum
end;
suppose A92: ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) ; :: thesis: x in Cl P1
now :: thesis: p in Cl P1
per cases ( ( p `2 = t2 & p `1 < s2 & p `1 > s1 ) or ( p `2 = t2 & p `1 = s1 ) or ( p `2 = t2 & p `1 = s2 ) ) by A92, XXREAL_0:1;
suppose A93: ( p `2 = t2 & p `1 < s2 & p `1 > s1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A94: Q is open and
A95: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A94, Lm9, PRE_TOPC:30;
then consider r being Real such that
A96: r > 0 and
A97: Ball (q,r) c= Q by A95, TOPMETR:15;
reconsider r = r as Real ;
A98: r / 2 > 0 by A96, XREAL_1:215;
A99: r / 2 < r by A96, XREAL_1:216;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A100: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= r / 2 by XXREAL_0:17;
A101: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
then A102: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A101, XXREAL_0:2;
A103: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < r by A99, A100, XXREAL_0:2;
A104: s2 - s1 > 0 by A1, XREAL_1:50;
A105: t2 - t1 > 0 by A2, XREAL_1:50;
A106: (s2 - s1) / 2 > 0 by A104, XREAL_1:215;
(t2 - t1) / 2 > 0 by A105, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A106, XXREAL_0:15;
then A107: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A98, XXREAL_0:15;
set pa = |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A108: |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = p `1 by EUCLID:52;
A109: |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
(t2 - t1) / 2 < t2 - t1 by A105, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `2) - t1 by A93, A102, XXREAL_0:2;
then A110: t1 < |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 by A109, XREAL_1:12;
|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A93, A107, A109, XREAL_1:44;
then A111: |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A93, A108, A110;
reconsider qa = |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A112: 0 <= ((p `1) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A113: 0 + 0 <= (((p `1) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A112, XREAL_1:7;
(((p `1) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A103, A107, A108, A109, SQUARE_1:16;
then (sqrt ((((p `1) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A113, SQUARE_1:def 2;
then A114: sqrt ((((p `1) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A96, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A114, TOPREAL3:7;
then |[(p `1),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A97, A111, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A115: ( p `2 = t2 & p `1 = s1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A116: Q is open and
A117: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A116, Lm9, PRE_TOPC:30;
then consider r being Real such that
A118: r > 0 and
A119: Ball (q,r) c= Q by A117, TOPMETR:15;
reconsider r = r as Real ;
A120: r / 2 > 0 by A118, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A121: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A122: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A123: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A124: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A121, A122, XXREAL_0:2;
A125: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A121, A123, XXREAL_0:2;
A126: s2 - s1 > 0 by A1, XREAL_1:50;
A127: t2 - t1 > 0 by A2, XREAL_1:50;
A128: (s2 - s1) / 2 > 0 by A126, XREAL_1:215;
(t2 - t1) / 2 > 0 by A127, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A128, XXREAL_0:15;
then A129: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A120, XXREAL_0:15;
set pa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A130: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A131: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A132: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A115, A129, A130, XREAL_1:29;
A133: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A115, A129, A131, XREAL_1:44;
(t2 - t1) / 2 < t2 - t1 by A127, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `2) - t1 by A115, A125, XXREAL_0:2;
then A134: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A131, XREAL_1:12;
(s2 - s1) / 2 < s2 - s1 by A126, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < s2 - (p `1) by A115, A124, XXREAL_0:2;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A130, XREAL_1:20;
then A135: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A132, A133, A134;
reconsider qa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A136: 0 <= ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A137: 0 + 0 <= (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A136, XREAL_1:7;
((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 <= (r / 2) ^2 by A129, A131, SQUARE_1:15, XXREAL_0:17;
then A138: (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A130, A131, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A118, A120, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A138, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A137, SQUARE_1:def 2;
then A139: sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A118, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A139, TOPREAL3:7;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A119, A135, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A140: ( p `2 = t2 & p `1 = s2 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A141: Q is open and
A142: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A141, Lm9, PRE_TOPC:30;
then consider r being Real such that
A143: r > 0 and
A144: Ball (q,r) c= Q by A142, TOPMETR:15;
reconsider r = r as Real ;
A145: r / 2 > 0 by A143, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A146: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A147: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A148: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A149: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A146, A147, XXREAL_0:2;
A150: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A146, A148, XXREAL_0:2;
A151: s2 - s1 > 0 by A1, XREAL_1:50;
A152: t2 - t1 > 0 by A2, XREAL_1:50;
A153: (s2 - s1) / 2 > 0 by A151, XREAL_1:215;
(t2 - t1) / 2 > 0 by A152, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A153, XXREAL_0:15;
then A154: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A145, XXREAL_0:15;
set pa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A155: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A156: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A157: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A140, A154, A155, XREAL_1:44;
A158: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A140, A154, A156, XREAL_1:44;
(s2 - s1) / 2 < s2 - s1 by A151, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `1) - s1 by A140, A149, XXREAL_0:2;
then A159: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A155, XREAL_1:12;
(t2 - t1) / 2 < t2 - t1 by A152, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `2) - t1 by A140, A150, XXREAL_0:2;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A156, XREAL_1:12;
then A160: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A157, A158, A159;
reconsider qa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A161: 0 <= ((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A162: 0 + 0 <= (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A161, XREAL_1:7;
(min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) ^2 <= (r / 2) ^2 by A154, SQUARE_1:15, XXREAL_0:17;
then A163: (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A155, A156, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A143, A145, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A163, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A162, SQUARE_1:def 2;
then A164: sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A143, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A164, TOPREAL3:7;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A144, A160, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
end;
end;
hence x in Cl P1 by A16; :: thesis: verum
end;
suppose A165: ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) ; :: thesis: x in Cl P1
now :: thesis: p in Cl P1
per cases ( ( p `2 = t1 & p `1 < s2 & p `1 > s1 ) or ( p `2 = t1 & p `1 = s1 ) or ( p `2 = t1 & p `1 = s2 ) ) by A165, XXREAL_0:1;
suppose A166: ( p `2 = t1 & p `1 < s2 & p `1 > s1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A167: Q is open and
A168: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A167, Lm9, PRE_TOPC:30;
then consider r being Real such that
A169: r > 0 and
A170: Ball (q,r) c= Q by A168, TOPMETR:15;
reconsider r = r as Real ;
A171: r / 2 > 0 by A169, XREAL_1:215;
A172: r / 2 < r by A169, XREAL_1:216;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A173: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= r / 2 by XXREAL_0:17;
A174: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
then A175: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A174, XXREAL_0:2;
A176: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < r by A172, A173, XXREAL_0:2;
A177: s2 - s1 > 0 by A1, XREAL_1:50;
A178: t2 - t1 > 0 by A2, XREAL_1:50;
A179: (s2 - s1) / 2 > 0 by A177, XREAL_1:215;
(t2 - t1) / 2 > 0 by A178, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A179, XXREAL_0:15;
then A180: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A171, XXREAL_0:15;
set pa = |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A181: |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A182: |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = p `1 by EUCLID:52;
(t2 - t1) / 2 < t2 - t1 by A178, XREAL_1:216;
then A183: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < t2 - (p `2) by A166, A175, XXREAL_0:2;
A184: t1 < |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 by A166, A180, A181, XREAL_1:29;
|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A181, A183, XREAL_1:20;
then A185: |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A166, A182, A184;
reconsider qa = |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A186: 0 <= ((p `1) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A187: 0 + 0 <= (((p `1) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A186, XREAL_1:7;
((|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2) - (p `2)) ^2 = ((p `2) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 ;
then (((p `1) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A176, A180, A181, A182, SQUARE_1:16;
then (sqrt ((((p `1) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A187, SQUARE_1:def 2;
then A188: sqrt ((((p `1) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A169, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A188, TOPREAL3:7;
then |[(p `1),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A170, A185, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A189: ( p `2 = t1 & p `1 = s1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A190: Q is open and
A191: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A190, Lm9, PRE_TOPC:30;
then consider r being Real such that
A192: r > 0 and
A193: Ball (q,r) c= Q by A191, TOPMETR:15;
reconsider r = r as Real ;
A194: r / 2 > 0 by A192, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A195: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A196: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A197: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A198: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A195, A196, XXREAL_0:2;
A199: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A195, A197, XXREAL_0:2;
A200: s2 - s1 > 0 by A1, XREAL_1:50;
A201: t2 - t1 > 0 by A2, XREAL_1:50;
A202: (s2 - s1) / 2 > 0 by A200, XREAL_1:215;
(t2 - t1) / 2 > 0 by A201, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A202, XXREAL_0:15;
then A203: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A194, XXREAL_0:15;
set pa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A204: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A205: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A206: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A189, A203, A204, XREAL_1:29;
A207: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A189, A203, A205, XREAL_1:29;
(s2 - s1) / 2 < s2 - s1 by A200, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < s2 - (p `1) by A189, A198, XXREAL_0:2;
then A208: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A204, XREAL_1:20;
(t2 - t1) / 2 < t2 - t1 by A201, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < t2 - (p `2) by A189, A199, XXREAL_0:2;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A205, XREAL_1:20;
then A209: |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A206, A207, A208;
reconsider qa = |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A210: 0 <= ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A211: 0 + 0 <= (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A210, XREAL_1:7;
((|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1) - (p `1)) ^2 = ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 ;
then ((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 <= (r / 2) ^2 by A203, A204, SQUARE_1:15, XXREAL_0:17;
then A212: (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A204, A205, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A192, A194, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A212, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A211, SQUARE_1:def 2;
then A213: sqrt ((((p `1) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A192, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A213, TOPREAL3:7;
then |[((p `1) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A193, A209, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A214: ( p `2 = t1 & p `1 = s2 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A215: Q is open and
A216: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A215, Lm9, PRE_TOPC:30;
then consider r being Real such that
A217: r > 0 and
A218: Ball (q,r) c= Q by A216, TOPMETR:15;
reconsider r = r as Real ;
A219: r / 2 > 0 by A217, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A220: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A221: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A222: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A223: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A220, A221, XXREAL_0:2;
A224: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A220, A222, XXREAL_0:2;
A225: s2 - s1 > 0 by A1, XREAL_1:50;
A226: t2 - t1 > 0 by A2, XREAL_1:50;
A227: (s2 - s1) / 2 > 0 by A225, XREAL_1:215;
(t2 - t1) / 2 > 0 by A226, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A227, XXREAL_0:15;
then A228: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A219, XXREAL_0:15;
set pa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A229: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A230: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
then A231: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A214, A228, XREAL_1:29;
A232: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A214, A228, A229, XREAL_1:44;
(t2 - t1) / 2 < t2 - t1 by A226, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < t2 - (p `2) by A214, A224, XXREAL_0:2;
then A233: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A230, XREAL_1:20;
(s2 - s1) / 2 < s2 - s1 by A225, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `1) - s1 by A214, A223, XXREAL_0:2;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A229, XREAL_1:12;
then A234: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A231, A232, A233;
reconsider qa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A235: 0 <= ((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A236: 0 + 0 <= (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A235, XREAL_1:7;
(min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) ^2 <= (r / 2) ^2 by A228, SQUARE_1:15, XXREAL_0:17;
then A237: (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A229, A230, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A217, A219, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A237, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A236, SQUARE_1:def 2;
then A238: sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A217, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A238, TOPREAL3:7;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A218, A234, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
end;
end;
hence x in Cl P1 by A16; :: thesis: verum
end;
suppose A239: ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ; :: thesis: x in Cl P1
now :: thesis: p in Cl P1
per cases ( ( p `1 = s2 & p `2 < t2 & p `2 > t1 ) or ( p `1 = s2 & p `2 = t1 ) or ( p `1 = s2 & p `2 = t2 ) ) by A239, XXREAL_0:1;
suppose A240: ( p `1 = s2 & p `2 < t2 & p `2 > t1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A241: Q is open and
A242: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A241, Lm9, PRE_TOPC:30;
then consider r being Real such that
A243: r > 0 and
A244: Ball (q,r) c= Q by A242, TOPMETR:15;
reconsider r = r as Real ;
A245: r / 2 > 0 by A243, XREAL_1:215;
A246: r / 2 < r by A243, XREAL_1:216;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A247: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= r / 2 by XXREAL_0:17;
A248: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
then A249: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A248, XXREAL_0:2;
A250: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < r by A246, A247, XXREAL_0:2;
A251: s2 - s1 > 0 by A1, XREAL_1:50;
A252: t2 - t1 > 0 by A2, XREAL_1:50;
A253: (s2 - s1) / 2 > 0 by A251, XREAL_1:215;
(t2 - t1) / 2 > 0 by A252, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A253, XXREAL_0:15;
then A254: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A245, XXREAL_0:15;
set pa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]|;
A255: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2 = p `2 by EUCLID:52;
A256: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1 = (p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
(s2 - s1) / 2 < s2 - s1 by A251, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `1) - s1 by A240, A249, XXREAL_0:2;
then A257: s1 < |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1 by A256, XREAL_1:12;
|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1 < s2 by A240, A254, A256, XREAL_1:44;
then A258: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| in P1 by A4, A240, A255, A257;
reconsider qa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| as Point of (Euclid 2) by EUCLID:22;
A259: 0 <= ((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2 by XREAL_1:63;
then A260: 0 + 0 <= (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2) by A259, XREAL_1:7;
(((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2) < r ^2 by A250, A254, A255, A256, SQUARE_1:16;
then (sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2))) ^2 < r ^2 by A260, SQUARE_1:def 2;
then A261: sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| `2)) ^2)) < r by A243, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A261, TOPREAL3:7;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),(p `2)]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A244, A258, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A262: ( p `1 = s2 & p `2 = t1 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A263: Q is open and
A264: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A263, Lm9, PRE_TOPC:30;
then consider r being Real such that
A265: r > 0 and
A266: Ball (q,r) c= Q by A264, TOPMETR:15;
reconsider r = r as Real ;
A267: r / 2 > 0 by A265, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A268: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A269: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A270: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A271: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A268, A269, XXREAL_0:2;
A272: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A268, A270, XXREAL_0:2;
A273: s2 - s1 > 0 by A1, XREAL_1:50;
A274: t2 - t1 > 0 by A2, XREAL_1:50;
A275: (s2 - s1) / 2 > 0 by A273, XREAL_1:215;
(t2 - t1) / 2 > 0 by A274, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A275, XXREAL_0:15;
then A276: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A267, XXREAL_0:15;
set pa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A277: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A278: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A279: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A262, A276, A277, XREAL_1:29;
A280: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A262, A276, A278, XREAL_1:44;
(s2 - s1) / 2 < s2 - s1 by A273, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `1) - s1 by A262, A271, XXREAL_0:2;
then A281: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A278, XREAL_1:12;
(t2 - t1) / 2 < t2 - t1 by A274, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < t2 - (p `2) by A262, A272, XXREAL_0:2;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A277, XREAL_1:20;
then A282: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A279, A280, A281;
reconsider qa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A283: 0 <= ((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A284: 0 + 0 <= (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A283, XREAL_1:7;
((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 <= (r / 2) ^2 by A276, A278, SQUARE_1:15, XXREAL_0:17;
then A285: (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A277, A278, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A265, A267, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A285, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A284, SQUARE_1:def 2;
then A286: sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A265, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A286, TOPREAL3:7;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) + (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A266, A282, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
suppose A287: ( p `1 = s2 & p `2 = t2 ) ; :: thesis: p in Cl P1
for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P1 meets Q
proof
let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P1 meets Q )
assume that
A288: Q is open and
A289: p in Q ; :: thesis: P1 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A288, Lm9, PRE_TOPC:30;
then consider r being Real such that
A290: r > 0 and
A291: Ball (q,r) c= Q by A289, TOPMETR:15;
reconsider r = r as Real ;
A292: r / 2 > 0 by A290, XREAL_1:215;
set r2 = min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))));
A293: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= min (((s2 - s1) / 2),((t2 - t1) / 2)) by XXREAL_0:17;
A294: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (s2 - s1) / 2 by XXREAL_0:17;
A295: min (((s2 - s1) / 2),((t2 - t1) / 2)) <= (t2 - t1) / 2 by XXREAL_0:17;
A296: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (s2 - s1) / 2 by A293, A294, XXREAL_0:2;
A297: min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) <= (t2 - t1) / 2 by A293, A295, XXREAL_0:2;
A298: s2 - s1 > 0 by A1, XREAL_1:50;
A299: t2 - t1 > 0 by A2, XREAL_1:50;
A300: (s2 - s1) / 2 > 0 by A298, XREAL_1:215;
(t2 - t1) / 2 > 0 by A299, XREAL_1:215;
then 0 < min (((s2 - s1) / 2),((t2 - t1) / 2)) by A300, XXREAL_0:15;
then A301: 0 < min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) by A292, XXREAL_0:15;
set pa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]|;
A302: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 = (p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A303: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 = (p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) by EUCLID:52;
A304: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 < s2 by A287, A301, A302, XREAL_1:44;
A305: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 < t2 by A287, A301, A303, XREAL_1:44;
(s2 - s1) / 2 < s2 - s1 by A298, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `1) - s1 by A287, A296, XXREAL_0:2;
then A306: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1 > s1 by A302, XREAL_1:12;
(t2 - t1) / 2 < t2 - t1 by A299, XREAL_1:216;
then min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))) < (p `2) - t1 by A287, A297, XXREAL_0:2;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2 > t1 by A303, XREAL_1:12;
then A307: |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in P1 by A4, A304, A305, A306;
reconsider qa = |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| as Point of (Euclid 2) by EUCLID:22;
A308: 0 <= ((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2 by XREAL_1:63;
then A309: 0 + 0 <= (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) by A308, XREAL_1:7;
(min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))) ^2 <= (r / 2) ^2 by A301, SQUARE_1:15, XXREAL_0:17;
then A310: (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A302, A303, XREAL_1:7;
r ^2 = (((r / 2) ^2) + ((r / 2) ^2)) + ((2 * (r / 2)) * (r / 2)) ;
then r ^2 > ((r / 2) ^2) + ((r / 2) ^2) by A290, A292, XREAL_1:29, XREAL_1:129;
then (((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2) < r ^2 by A310, XXREAL_0:2;
then (sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2))) ^2 < r ^2 by A309, SQUARE_1:def 2;
then A311: sqrt ((((p `1) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `1)) ^2) + (((p `2) - (|[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| `2)) ^2)) < r by A290, SQUARE_1:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A311, TOPREAL3:7;
then |[((p `1) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2)))))),((p `2) - (min ((r / 2),(min (((s2 - s1) / 2),((t2 - t1) / 2))))))]| in Ball (q,r) by METRIC_1:11;
hence P1 meets Q by A291, A307, XBOOLE_0:3; :: thesis: verum
end;
hence p in Cl P1 by PRE_TOPC:def 7; :: thesis: verum
end;
end;
end;
hence x in Cl P1 by A16; :: thesis: verum
end;
end;
end;
hence x in Cl P1 ; :: thesis: verum
end;
hence P \/ P1 c= Cl P1 by A5, XBOOLE_1:8; :: thesis: verum