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 Th35;
A5: P1 c= Cl P1 by PRE_TOPC:48;
reconsider PP = P ` as Subset of (TOP-REAL 2) ;
A6: PP = P1 \/ P2 by A1, A2, A3, A4, Th41;
P1 misses P2 by A1, A2, A3, A4, Th41;
then A7: P1 c= P2 ` by SUBSET_1:43;
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:18;
then A9: [#] (TOP-REAL 2) = (P \/ P1) \/ P2 by XBOOLE_1:4;

now

let x be set ; :: 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 by TARSKI:def 3;

now

let x be set ; :: 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 ` by TARSKI:def 3;
then A12: P2 ` = P \/ P1 by A11, XBOOLE_0:def 10;
A13: P2 is open by Th39;
([#] (TOP-REAL 2)) \ (P2 ` ) = (P2 ` ) `
.= P2 ;
then A14: P \/ P1 is closed by A12, A13, PRE_TOPC:def 6;
A15: P1 c= P \/ P1 by XBOOLE_1:7;
thus Cl P1 c= P \/ P1 :: according to XBOOLE_0:def 10 :: thesis: P \/ P1 c= Cl P1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl P1 or x in P \/ P1 )
assume x in Cl P1 ; :: thesis: x in P \/ P1
hence x in P \/ P1 by A14, A15, PRE_TOPC:45; :: thesis: verum

end;

P c= Cl P1

proof

let x be set ; :: 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:25;

now

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

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:60;
then consider r being real number such that
A22: r > 0 and
A23: Ball q,r c= Q by A21, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A24: r / 2 > 0 by A22, XREAL_1:217;
A25: r / 2 < r by A22, XREAL_1:218;
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:52;
A31: t2 - t1 > 0 by A2, XREAL_1:52;
A32: (s2 - s1) / 2 > 0 by A30, XREAL_1:217;
(t2 - t1) / 2 > 0 by A31, XREAL_1:217;
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:56;
A35: |[((p `1 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `2 = p `2 by EUCLID:56;
(s2 - s1) / 2 < s2 - s1 by A30, XREAL_1:218;
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:31;
|[((p `1 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `1 < s2 by A34, A36, XREAL_1:22;
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:25;
A39: 0 <= ((p `1 ) - (|[((p `1 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[((p `1 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `2 )) ^2 by XREAL_1:65;
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:9;
((|[((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:78;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A41, TOPREAL3:12;
then |[((p `1 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| in Ball q,r by METRIC_1:12;
hence P1 meets Q by A23, A38, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A45: r > 0 and
A46: Ball q,r c= Q by A44, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A47: r / 2 > 0 by A45, XREAL_1:217;
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:52;
A54: t2 - t1 > 0 by A2, XREAL_1:52;
A55: (s2 - s1) / 2 > 0 by A53, XREAL_1:217;
(t2 - t1) / 2 > 0 by A54, XREAL_1:217;
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:56;
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:56;
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:31;
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:31;
(s2 - s1) / 2 < s2 - s1 by A53, XREAL_1:218;
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:22;
(t2 - t1) / 2 < t2 - t1 by A54, XREAL_1:218;
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:22;
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:25;
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:65;
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:65;
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:9;
((|[((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:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A66, TOPREAL3:12;
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:12;
hence P1 meets Q by A46, A62, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A70: r > 0 and
A71: Ball q,r c= Q by A69, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A72: r / 2 > 0 by A70, XREAL_1:217;
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:52;
A79: t2 - t1 > 0 by A2, XREAL_1:52;
A80: (s2 - s1) / 2 > 0 by A78, XREAL_1:217;
(t2 - t1) / 2 > 0 by A79, XREAL_1:217;
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:56;
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:56;
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:31;
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:46;
(s2 - s1) / 2 < s2 - s1 by A78, XREAL_1:218;
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:22;
(t2 - t1) / 2 < t2 - t1 by A79, XREAL_1:218;
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:14;
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:25;
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:65;
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:65;
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:9;
(min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))) ^2 <= (r / 2) ^2 by A81, SQUARE_1:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A91, TOPREAL3:12;
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:12;
hence P1 meets Q by A71, A87, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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

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:60;
then consider r being real number such that
A96: r > 0 and
A97: Ball q,r c= Q by A95, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A98: r / 2 > 0 by A96, XREAL_1:217;
A99: r / 2 < r by A96, XREAL_1:218;
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:52;
A105: t2 - t1 > 0 by A2, XREAL_1:52;
A106: (s2 - s1) / 2 > 0 by A104, XREAL_1:217;
(t2 - t1) / 2 > 0 by A105, XREAL_1:217;
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:56;
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:56;
(t2 - t1) / 2 < t2 - t1 by A105, XREAL_1:218;
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:14;
|[(p `1 ),((p `2 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `2 < t2 by A93, A107, A109, XREAL_1:46;
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:25;
A112: 0 <= ((p `1 ) - (|[(p `1 ),((p `2 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[(p `1 ),((p `2 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `2 )) ^2 by XREAL_1:65;
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:9;
(((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:78;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A114, TOPREAL3:12;
then |[(p `1 ),((p `2 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| in Ball q,r by METRIC_1:12;
hence P1 meets Q by A97, A111, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A118: r > 0 and
A119: Ball q,r c= Q by A117, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A120: r / 2 > 0 by A118, XREAL_1:217;
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:52;
A127: t2 - t1 > 0 by A2, XREAL_1:52;
A128: (s2 - s1) / 2 > 0 by A126, XREAL_1:217;
(t2 - t1) / 2 > 0 by A127, XREAL_1:217;
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:56;
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:56;
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:31;
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:46;
(t2 - t1) / 2 < t2 - t1 by A127, XREAL_1:218;
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:14;
(s2 - s1) / 2 < s2 - s1 by A126, XREAL_1:218;
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:22;
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:25;
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:65;
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:65;
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:9;
((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:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A139, TOPREAL3:12;
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:12;
hence P1 meets Q by A119, A135, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A143: r > 0 and
A144: Ball q,r c= Q by A142, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A145: r / 2 > 0 by A143, XREAL_1:217;
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:52;
A152: t2 - t1 > 0 by A2, XREAL_1:52;
A153: (s2 - s1) / 2 > 0 by A151, XREAL_1:217;
(t2 - t1) / 2 > 0 by A152, XREAL_1:217;
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:56;
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:56;
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:46;
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:46;
(s2 - s1) / 2 < s2 - s1 by A151, XREAL_1:218;
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:14;
(t2 - t1) / 2 < t2 - t1 by A152, XREAL_1:218;
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:14;
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:25;
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:65;
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:65;
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:9;
(min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))) ^2 <= (r / 2) ^2 by A154, SQUARE_1:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A164, TOPREAL3:12;
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:12;
hence P1 meets Q by A144, A160, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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

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:60;
then consider r being real number such that
A169: r > 0 and
A170: Ball q,r c= Q by A168, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A171: r / 2 > 0 by A169, XREAL_1:217;
A172: r / 2 < r by A169, XREAL_1:218;
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:52;
A178: t2 - t1 > 0 by A2, XREAL_1:52;
A179: (s2 - s1) / 2 > 0 by A177, XREAL_1:217;
(t2 - t1) / 2 > 0 by A178, XREAL_1:217;
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:56;
A182: |[(p `1 ),((p `2 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `1 = p `1 by EUCLID:56;
(t2 - t1) / 2 < t2 - t1 by A178, XREAL_1:218;
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:31;
|[(p `1 ),((p `2 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `2 < t2 by A181, A183, XREAL_1:22;
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:25;
A186: 0 <= ((p `1 ) - (|[(p `1 ),((p `2 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[(p `1 ),((p `2 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| `2 )) ^2 by XREAL_1:65;
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:9;
((|[(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:78;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A188, TOPREAL3:12;
then |[(p `1 ),((p `2 ) + (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))))]| in Ball q,r by METRIC_1:12;
hence P1 meets Q by A170, A185, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A192: r > 0 and
A193: Ball q,r c= Q by A191, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A194: r / 2 > 0 by A192, XREAL_1:217;
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:52;
A201: t2 - t1 > 0 by A2, XREAL_1:52;
A202: (s2 - s1) / 2 > 0 by A200, XREAL_1:217;
(t2 - t1) / 2 > 0 by A201, XREAL_1:217;
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:56;
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:56;
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:31;
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:31;
(s2 - s1) / 2 < s2 - s1 by A200, XREAL_1:218;
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:22;
(t2 - t1) / 2 < t2 - t1 by A201, XREAL_1:218;
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:22;
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:25;
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:65;
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:65;
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:9;
((|[((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:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A213, TOPREAL3:12;
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:12;
hence P1 meets Q by A193, A209, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A217: r > 0 and
A218: Ball q,r c= Q by A216, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A219: r / 2 > 0 by A217, XREAL_1:217;
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:52;
A226: t2 - t1 > 0 by A2, XREAL_1:52;
A227: (s2 - s1) / 2 > 0 by A225, XREAL_1:217;
(t2 - t1) / 2 > 0 by A226, XREAL_1:217;
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:56;
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:56;
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:31;
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:46;
(t2 - t1) / 2 < t2 - t1 by A226, XREAL_1:218;
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:22;
(s2 - s1) / 2 < s2 - s1 by A225, XREAL_1:218;
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:14;
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:25;
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:65;
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:65;
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:9;
(min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))) ^2 <= (r / 2) ^2 by A228, SQUARE_1:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A238, TOPREAL3:12;
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:12;
hence P1 meets Q by A218, A234, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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

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:60;
then consider r being real number such that
A243: r > 0 and
A244: Ball q,r c= Q by A242, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A245: r / 2 > 0 by A243, XREAL_1:217;
A246: r / 2 < r by A243, XREAL_1:218;
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:52;
A252: t2 - t1 > 0 by A2, XREAL_1:52;
A253: (s2 - s1) / 2 > 0 by A251, XREAL_1:217;
(t2 - t1) / 2 > 0 by A252, XREAL_1:217;
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:56;
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:56;
(s2 - s1) / 2 < s2 - s1 by A251, XREAL_1:218;
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:14;
|[((p `1 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `1 < s2 by A240, A254, A256, XREAL_1:46;
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:25;
A259: 0 <= ((p `1 ) - (|[((p `1 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[((p `1 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| `2 )) ^2 by XREAL_1:65;
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:9;
(((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:78;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A261, TOPREAL3:12;
then |[((p `1 ) - (min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2)))),(p `2 )]| in Ball q,r by METRIC_1:12;
hence P1 meets Q by A244, A258, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A265: r > 0 and
A266: Ball q,r c= Q by A264, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A267: r / 2 > 0 by A265, XREAL_1:217;
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:52;
A274: t2 - t1 > 0 by A2, XREAL_1:52;
A275: (s2 - s1) / 2 > 0 by A273, XREAL_1:217;
(t2 - t1) / 2 > 0 by A274, XREAL_1:217;
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:56;
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:56;
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:31;
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:46;
(s2 - s1) / 2 < s2 - s1 by A273, XREAL_1:218;
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:14;
(t2 - t1) / 2 < t2 - t1 by A274, XREAL_1:218;
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:22;
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:25;
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:65;
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:65;
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:9;
((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:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A286, TOPREAL3:12;
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:12;
hence P1 meets Q by A266, A282, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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:60;
then consider r being real number such that
A290: r > 0 and
A291: Ball q,r c= Q by A289, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A292: r / 2 > 0 by A290, XREAL_1:217;
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:52;
A299: t2 - t1 > 0 by A2, XREAL_1:52;
A300: (s2 - s1) / 2 > 0 by A298, XREAL_1:217;
(t2 - t1) / 2 > 0 by A299, XREAL_1:217;
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:56;
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:56;
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:46;
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:46;
(s2 - s1) / 2 < s2 - s1 by A298, XREAL_1:218;
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:14;
(t2 - t1) / 2 < t2 - t1 by A299, XREAL_1:218;
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:14;
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:25;
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:65;
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:65;
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:9;
(min (r / 2),(min ((s2 - s1) / 2),((t2 - t1) / 2))) ^2 <= (r / 2) ^2 by A301, SQUARE_1:77, 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:9;
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:31, XREAL_1:131;
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 4;
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:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A311, TOPREAL3:12;
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:12;
hence P1 meets Q by A291, A307, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl P1 by PRE_TOPC:def 13; :: 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