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:18;
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 Th23;
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: P2 c= P1 ` by SUBSET_1:23;
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:2
.= (P \/ P2) \/ P1 by XBOOLE_1:4 ;
now :: thesis: for x being object st x in P1 ` holds
x in P \/ P2
let x be object ; :: 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 ;
now :: thesis: for x being object st x in P \/ P2 holds
x in P1 `
let x be object ; :: 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 ` ;
then A12: P1 ` = P \/ P2 by A11;
A13: P1 is open by Th27;
([#] (TOP-REAL 2)) \ (P1 `) = (P1 `) `
.= P1 ;
then A14: P \/ P2 is closed by A12, A13, PRE_TOPC:def 3;
A15: P2 c= P \/ P2 by XBOOLE_1:7;
thus Cl P2 c= P \/ P2 by A14, A15, PRE_TOPC:15; :: according to XBOOLE_0:def 10 :: thesis: P \/ P2 c= Cl P2
P c= Cl P2
proof
let x be object ; :: 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:22;
now :: thesis: x in Cl P2
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:30;
then consider r being Real such that
A21: r > 0 and
A22: Ball (q,r) c= Q by A20, TOPMETR:15;
reconsider r = r as Real ;
set pa = |[((p `1) - (r / 2)),(p `2)]|;
A23: |[((p `1) - (r / 2)),(p `2)]| `1 = (p `1) - (r / 2) by EUCLID:52;
A24: |[((p `1) - (r / 2)),(p `2)]| `2 = p `2 by EUCLID:52;
A25: r / 2 > 0 by A21, XREAL_1:215;
( 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:44, XREAL_1:215;
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:22;
A27: 0 <= ((p `1) - (|[((p `1) - (r / 2)),(p `2)]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) - (r / 2)),(p `2)]| `2)) ^2 by XREAL_1:63;
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:7;
(p `1) - (|[((p `1) - (r / 2)),(p `2)]| `1) < r by A21, A23, XREAL_1:216;
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:16;
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 2;
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:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A29, TOPREAL3:7;
then |[((p `1) - (r / 2)),(p `2)]| in Ball (q,r) by METRIC_1:11;
then P2 /\ Q <> {} by A22, A26, XBOOLE_0:def 4;
hence P2 meets Q ; :: thesis: verum
end;
hence x in Cl P2 by A16, PRE_TOPC:def 7; :: 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:30;
then consider r being Real such that
A33: r > 0 and
A34: Ball (q,r) c= Q by A32, TOPMETR:15;
reconsider r = r as Real ;
set pa = |[(p `1),((p `2) + (r / 2))]|;
A35: |[(p `1),((p `2) + (r / 2))]| `1 = p `1 by EUCLID:52;
A36: |[(p `1),((p `2) + (r / 2))]| `2 = (p `2) + (r / 2) by EUCLID:52;
A37: r / 2 > 0 by A33, XREAL_1:215;
( 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:29, XREAL_1:215;
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:22;
A39: 0 <= ((p `1) - (|[(p `1),((p `2) + (r / 2))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[(p `1),((p `2) + (r / 2))]| `2)) ^2 by XREAL_1:63;
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:7;
A41: (|[(p `1),((p `2) + (r / 2))]| `2) - (p `2) < r by A33, A36, XREAL_1:216;
((|[(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:16;
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 2;
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:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A42, TOPREAL3:7;
then |[(p `1),((p `2) + (r / 2))]| in Ball (q,r) by METRIC_1:11;
then P2 /\ Q <> {} by A34, A38, XBOOLE_0:def 4;
hence P2 meets Q ; :: thesis: verum
end;
hence x in Cl P2 by A16, PRE_TOPC:def 7; :: 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:30;
then consider r being Real such that
A46: r > 0 and
A47: Ball (q,r) c= Q by A45, TOPMETR:15;
reconsider r = r as Real ;
set pa = |[(p `1),((p `2) - (r / 2))]|;
A48: |[(p `1),((p `2) - (r / 2))]| `1 = p `1 by EUCLID:52;
A49: |[(p `1),((p `2) - (r / 2))]| `2 = (p `2) - (r / 2) by EUCLID:52;
A50: r / 2 > 0 by A46, XREAL_1:215;
( 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:44, XREAL_1:215;
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:22;
A52: 0 <= ((p `1) - (|[(p `1),((p `2) - (r / 2))]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[(p `1),((p `2) - (r / 2))]| `2)) ^2 by XREAL_1:63;
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:7;
(p `2) - (|[(p `1),((p `2) - (r / 2))]| `2) < r by A46, A49, XREAL_1:216;
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:16;
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 2;
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:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A54, TOPREAL3:7;
then |[(p `1),((p `2) - (r / 2))]| in Ball (q,r) by METRIC_1:11;
hence P2 meets Q by A47, A51, XBOOLE_0:3; :: thesis: verum
end;
hence x in Cl P2 by A16, PRE_TOPC:def 7; :: 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:30;
then consider r being Real such that
A58: r > 0 and
A59: Ball (q,r) c= Q by A57, TOPMETR:15;
reconsider r = r as Real ;
set pa = |[((p `1) + (r / 2)),(p `2)]|;
A60: |[((p `1) + (r / 2)),(p `2)]| `1 = (p `1) + (r / 2) by EUCLID:52;
A61: |[((p `1) + (r / 2)),(p `2)]| `2 = p `2 by EUCLID:52;
A62: r / 2 > 0 by A58, XREAL_1:215;
( 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:29, XREAL_1:215;
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:22;
A64: 0 <= ((p `1) - (|[((p `1) + (r / 2)),(p `2)]| `1)) ^2 by XREAL_1:63;
0 <= ((p `2) - (|[((p `1) + (r / 2)),(p `2)]| `2)) ^2 by XREAL_1:63;
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:7;
A66: (|[((p `1) + (r / 2)),(p `2)]| `1) - (p `1) < r by A58, A60, XREAL_1:216;
((|[((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:16;
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 2;
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:15;
(Pitag_dist 2) . (q,qa) = dist (q,qa) by METRIC_1:def 1;
then dist (q,qa) < r by A67, TOPREAL3:7;
then |[((p `1) + (r / 2)),(p `2)]| in Ball (q,r) by METRIC_1:11;
hence P2 meets Q by A59, A63, XBOOLE_0:3; :: thesis: verum
end;
hence x in Cl P2 by A16, PRE_TOPC:def 7; :: 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