let s1, t1, s2, t2 be Real; :: thesis: for P, P2 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 ) ) } & 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 ) } holds
Cl P2 = P \/ P2
let P, P2 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 ) ) } & 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 ) } implies Cl P2 = P \/ P2 )
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: 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 ) } ; :: thesis: Cl P2 = P \/ P2
A5: P2 c= Cl P2 by PRE_TOPC:48;
reconsider P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } as Subset of (TOP-REAL 2) by Th34;
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: P2 c= P1 ` by SUBSET_1:43;
P = (P1 \/ P2) ` by A6;
then A8: P = (([#] (TOP-REAL 2)) \ P1) /\ (([#] (TOP-REAL 2)) \ P2) by XBOOLE_1:53;
A9: [#] (TOP-REAL 2) = P \/ (P2 \/ P1) by A6, PRE_TOPC:18
.= (P \/ P2) \/ P1 by XBOOLE_1:4 ;

now

let x be set ; :: thesis: ( x in P1 ` implies x in P \/ P2 )
assume A10: x in P1 ` ; :: thesis: x in P \/ P2
then not x in P1 by XBOOLE_0:def 5;
hence x in P \/ P2 by A9, A10, XBOOLE_0:def 3; :: thesis: verum

end;

then A11: P1 ` c= P \/ P2 by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in P \/ P2 implies x in P1 ` )
assume x in P \/ P2 ; :: thesis: x in P1 `
then ( x in P or x in P2 ) by XBOOLE_0:def 3;
hence x in P1 ` by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

then P \/ P2 c= P1 ` by TARSKI:def 3;
then A12: P1 ` = P \/ P2 by A11, XBOOLE_0:def 10;
A13: P1 is open by Th38;
([#] (TOP-REAL 2)) \ (P1 ` ) = (P1 ` ) `
.= P1 ;
then A14: P \/ P2 is closed by A12, A13, PRE_TOPC:def 6;
A15: P2 c= P \/ P2 by XBOOLE_1:7;
thus Cl P2 c= P \/ P2 :: according to XBOOLE_0:def 10 :: thesis: P \/ P2 c= Cl P2

proof

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

end;

P c= Cl P2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in Cl P2 )
assume x in P ; :: thesis: x in Cl P2
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 P2

for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P2 meets Q

proof

let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P2 meets Q )
assume that
A19: Q is open and
A20: p in Q ; :: thesis: P2 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A19, Lm9, PRE_TOPC:60;
then consider r being real number such that
A21: r > 0 and
A22: Ball q,r c= Q by A20, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
set pa = |[((p `1 ) - (r / 2)),(p `2 )]|;
A23: |[((p `1 ) - (r / 2)),(p `2 )]| `1 = (p `1 ) - (r / 2) by EUCLID:56;
A24: |[((p `1 ) - (r / 2)),(p `2 )]| `2 = p `2 by EUCLID:56;
A25: r / 2 > 0 by A21, XREAL_1:217;
( not s1 <= |[((p `1 ) - (r / 2)),(p `2 )]| `1 or not |[((p `1 ) - (r / 2)),(p `2 )]| `1 <= s2 or not t1 <= |[((p `1 ) - (r / 2)),(p `2 )]| `2 or not |[((p `1 ) - (r / 2)),(p `2 )]| `2 <= t2 ) by A18, A21, A23, XREAL_1:46, XREAL_1:217;
then A26: |[((p `1 ) - (r / 2)),(p `2 )]| in P2 by A4;
reconsider qa = |[((p `1 ) - (r / 2)),(p `2 )]| as Point of (Euclid 2) by EUCLID:25;
A27: 0 <= ((p `1 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 by XREAL_1:65;
then A28: 0 + 0 <= (((p `1 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 ) by A27, XREAL_1:9;
(p `1 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `1 ) < r by A21, A23, XREAL_1:218;
then (((p `1 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 ) < r ^2 by A23, A24, A25, SQUARE_1:78;
then (sqrt ((((p `1 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 ))) ^2 < r ^2 by A28, SQUARE_1:def 4;
then A29: sqrt ((((p `1 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) - (r / 2)),(p `2 )]| `2 )) ^2 )) < r by A21, SQUARE_1:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A29, TOPREAL3:12;
then |[((p `1 ) - (r / 2)),(p `2 )]| in Ball q,r by METRIC_1:12;
then P2 /\ Q <> {} by A22, A26, XBOOLE_0:def 4;
hence P2 meets Q by XBOOLE_0:def 7; :: thesis: verum

end;

hence x in Cl P2 by A16, PRE_TOPC:def 13; :: thesis: verum

end;

suppose A30: ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) ; :: thesis: x in Cl P2

for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P2 meets Q

proof

let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P2 meets Q )
assume that
A31: Q is open and
A32: p in Q ; :: thesis: P2 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A31, Lm9, PRE_TOPC:60;
then consider r being real number such that
A33: r > 0 and
A34: Ball q,r c= Q by A32, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
set pa = |[(p `1 ),((p `2 ) + (r / 2))]|;
A35: |[(p `1 ),((p `2 ) + (r / 2))]| `1 = p `1 by EUCLID:56;
A36: |[(p `1 ),((p `2 ) + (r / 2))]| `2 = (p `2 ) + (r / 2) by EUCLID:56;
A37: r / 2 > 0 by A33, XREAL_1:217;
( not s1 <= |[(p `1 ),((p `2 ) + (r / 2))]| `1 or not |[(p `1 ),((p `2 ) + (r / 2))]| `1 <= s2 or not t1 <= |[(p `1 ),((p `2 ) + (r / 2))]| `2 or not |[(p `1 ),((p `2 ) + (r / 2))]| `2 <= t2 ) by A30, A33, A36, XREAL_1:31, XREAL_1:217;
then A38: |[(p `1 ),((p `2 ) + (r / 2))]| in P2 by A4;
reconsider qa = |[(p `1 ),((p `2 ) + (r / 2))]| as Point of (Euclid 2) by EUCLID:25;
A39: 0 <= ((p `1 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `2 )) ^2 by XREAL_1:65;
then A40: 0 + 0 <= (((p `1 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `2 )) ^2 ) by A39, XREAL_1:9;
A41: (|[(p `1 ),((p `2 ) + (r / 2))]| `2 ) - (p `2 ) < r by A33, A36, XREAL_1:218;
((|[(p `1 ),((p `2 ) + (r / 2))]| `2 ) - (p `2 )) ^2 = ((p `2 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `2 )) ^2 ;
then (((p `1 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `2 )) ^2 ) < r ^2 by A35, A36, A37, A41, SQUARE_1:78;
then (sqrt ((((p `1 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `2 )) ^2 ))) ^2 < r ^2 by A40, SQUARE_1:def 4;
then A42: sqrt ((((p `1 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) + (r / 2))]| `2 )) ^2 )) < r by A33, SQUARE_1:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A42, TOPREAL3:12;
then |[(p `1 ),((p `2 ) + (r / 2))]| in Ball q,r by METRIC_1:12;
then P2 /\ Q <> {} by A34, A38, XBOOLE_0:def 4;
hence P2 meets Q by XBOOLE_0:def 7; :: thesis: verum

end;

hence x in Cl P2 by A16, PRE_TOPC:def 13; :: thesis: verum

end;

suppose A43: ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) ; :: thesis: x in Cl P2

for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P2 meets Q

proof

let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P2 meets Q )
assume that
A44: Q is open and
A45: p in Q ; :: thesis: P2 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A44, Lm9, PRE_TOPC:60;
then consider r being real number such that
A46: r > 0 and
A47: Ball q,r c= Q by A45, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
set pa = |[(p `1 ),((p `2 ) - (r / 2))]|;
A48: |[(p `1 ),((p `2 ) - (r / 2))]| `1 = p `1 by EUCLID:56;
A49: |[(p `1 ),((p `2 ) - (r / 2))]| `2 = (p `2 ) - (r / 2) by EUCLID:56;
A50: r / 2 > 0 by A46, XREAL_1:217;
( not s1 <= |[(p `1 ),((p `2 ) - (r / 2))]| `1 or not |[(p `1 ),((p `2 ) - (r / 2))]| `1 <= s2 or not t1 <= |[(p `1 ),((p `2 ) - (r / 2))]| `2 or not |[(p `1 ),((p `2 ) - (r / 2))]| `2 <= t2 ) by A43, A46, A49, XREAL_1:46, XREAL_1:217;
then A51: |[(p `1 ),((p `2 ) - (r / 2))]| in P2 by A4;
reconsider qa = |[(p `1 ),((p `2 ) - (r / 2))]| as Point of (Euclid 2) by EUCLID:25;
A52: 0 <= ((p `1 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `2 )) ^2 by XREAL_1:65;
then A53: 0 + 0 <= (((p `1 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `2 )) ^2 ) by A52, XREAL_1:9;
(p `2 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `2 ) < r by A46, A49, XREAL_1:218;
then (((p `1 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `2 )) ^2 ) < r ^2 by A48, A49, A50, SQUARE_1:78;
then (sqrt ((((p `1 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `2 )) ^2 ))) ^2 < r ^2 by A53, SQUARE_1:def 4;
then A54: sqrt ((((p `1 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `1 )) ^2 ) + (((p `2 ) - (|[(p `1 ),((p `2 ) - (r / 2))]| `2 )) ^2 )) < r by A46, SQUARE_1:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A54, TOPREAL3:12;
then |[(p `1 ),((p `2 ) - (r / 2))]| in Ball q,r by METRIC_1:12;
hence P2 meets Q by A47, A51, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl P2 by A16, PRE_TOPC:def 13; :: thesis: verum

end;

suppose A55: ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ; :: thesis: x in Cl P2

for Q being Subset of (TOP-REAL 2) st Q is open & p in Q holds
P2 meets Q

proof

let Q be Subset of (TOP-REAL 2); :: thesis: ( Q is open & p in Q implies P2 meets Q )
assume that
A56: Q is open and
A57: p in Q ; :: thesis: P2 meets Q
reconsider QQ = Q as Subset of (TopSpaceMetr (Euclid 2)) by Lm9;
QQ is open by A56, Lm9, PRE_TOPC:60;
then consider r being real number such that
A58: r > 0 and
A59: Ball q,r c= Q by A57, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
set pa = |[((p `1 ) + (r / 2)),(p `2 )]|;
A60: |[((p `1 ) + (r / 2)),(p `2 )]| `1 = (p `1 ) + (r / 2) by EUCLID:56;
A61: |[((p `1 ) + (r / 2)),(p `2 )]| `2 = p `2 by EUCLID:56;
A62: r / 2 > 0 by A58, XREAL_1:217;
( not s1 <= |[((p `1 ) + (r / 2)),(p `2 )]| `1 or not |[((p `1 ) + (r / 2)),(p `2 )]| `1 <= s2 or not t1 <= |[((p `1 ) + (r / 2)),(p `2 )]| `2 or not |[((p `1 ) + (r / 2)),(p `2 )]| `2 <= t2 ) by A55, A58, A60, XREAL_1:31, XREAL_1:217;
then A63: |[((p `1 ) + (r / 2)),(p `2 )]| in P2 by A4;
reconsider qa = |[((p `1 ) + (r / 2)),(p `2 )]| as Point of (Euclid 2) by EUCLID:25;
A64: 0 <= ((p `1 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `1 )) ^2 by XREAL_1:65;
0 <= ((p `2 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `2 )) ^2 by XREAL_1:65;
then A65: 0 + 0 <= (((p `1 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `2 )) ^2 ) by A64, XREAL_1:9;
A66: (|[((p `1 ) + (r / 2)),(p `2 )]| `1 ) - (p `1 ) < r by A58, A60, XREAL_1:218;
((|[((p `1 ) + (r / 2)),(p `2 )]| `1 ) - (p `1 )) ^2 = ((p `1 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `1 )) ^2 ;
then (((p `1 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `2 )) ^2 ) < r ^2 by A60, A61, A62, A66, SQUARE_1:78;
then (sqrt ((((p `1 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `2 )) ^2 ))) ^2 < r ^2 by A65, SQUARE_1:def 4;
then A67: sqrt ((((p `1 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `1 )) ^2 ) + (((p `2 ) - (|[((p `1 ) + (r / 2)),(p `2 )]| `2 )) ^2 )) < r by A58, SQUARE_1:77;
(Pitag_dist 2) . q,qa = dist q,qa by METRIC_1:def 1;
then dist q,qa < r by A67, TOPREAL3:12;
then |[((p `1 ) + (r / 2)),(p `2 )]| in Ball q,r by METRIC_1:12;
hence P2 meets Q by A59, A63, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl P2 by A16, PRE_TOPC:def 13; :: thesis: verum

end;

end;

end;

hence x in Cl P2 ; :: thesis: verum

end;

hence P \/ P2 c= Cl P2 by A5, XBOOLE_1:8; :: thesis: verum