let S, T be TopSpace; for A being Subset of S
for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]
let A be Subset of S; for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]
let B be Subset of T; Cl [:A,B:] = [:(Cl A),(Cl B):]
hereby TARSKI:def 3,
XBOOLE_0:def 10 [:(Cl A),(Cl B):] c= Cl [:A,B:]
let x be
object ;
( x in Cl [:A,B:] implies x in [:(Cl A),(Cl B):] )assume A1:
x in Cl [:A,B:]
;
x in [:(Cl A),(Cl B):]then reconsider S1 =
S,
T1 =
T as non
empty TopSpace ;
reconsider p =
x as
Point of
[:S1,T1:] by A1;
consider K being
Basis of
p such that A2:
for
Q being
Subset of
[:S1,T1:] st
Q in K holds
[:A,B:] meets Q
by A1, YELLOW13:17;
consider p1 being
Point of
S1,
p2 being
Point of
T1 such that A3:
p = [p1,p2]
by BORSUK_1:10;
for
G being
Subset of
T1 st
G is
open &
p2 in G holds
B meets G
proof
let G be
Subset of
T1;
( G is open & p2 in G implies B meets G )
assume
(
G is
open &
p2 in G )
;
B meets G
then
(
[p1,p2] in [:([#] S1),G:] &
[:([#] S1),G:] is
open )
by BORSUK_1:6, ZFMISC_1:87;
then consider V being
Subset of
[:S1,T1:] such that A4:
V in K
and A5:
V c= [:([#] S1),G:]
by A3, YELLOW_8:def 1;
[:A,B:] meets V
by A2, A4;
then consider a being
object such that A6:
(
a in [:A,B:] &
a in V )
by XBOOLE_0:3;
a in [:A,B:] /\ [:([#] S1),G:]
by A5, A6, XBOOLE_0:def 4;
then
a in [:(A /\ ([#] S1)),(B /\ G):]
by ZFMISC_1:100;
then
ex
a1,
a2 being
object st
(
a1 in A /\ ([#] S1) &
a2 in B /\ G &
a = [a1,a2] )
by ZFMISC_1:def 2;
hence
B meets G
;
verum
end; then A7:
p2 in Cl B
by PRE_TOPC:def 7;
for
G being
Subset of
S1 st
G is
open &
p1 in G holds
A meets G
proof
let G be
Subset of
S1;
( G is open & p1 in G implies A meets G )
assume
(
G is
open &
p1 in G )
;
A meets G
then
(
[p1,p2] in [:G,([#] T1):] &
[:G,([#] T1):] is
open )
by BORSUK_1:6, ZFMISC_1:87;
then consider V being
Subset of
[:S1,T1:] such that A8:
V in K
and A9:
V c= [:G,([#] T1):]
by A3, YELLOW_8:def 1;
[:A,B:] meets V
by A2, A8;
then consider a being
object such that A10:
(
a in [:A,B:] &
a in V )
by XBOOLE_0:3;
a in [:A,B:] /\ [:G,([#] T1):]
by A9, A10, XBOOLE_0:def 4;
then
a in [:(A /\ G),(B /\ ([#] T1)):]
by ZFMISC_1:100;
then
ex
a1,
a2 being
object st
(
a1 in A /\ G &
a2 in B /\ ([#] T1) &
a = [a1,a2] )
by ZFMISC_1:def 2;
hence
A meets G
;
verum
end; then
p1 in Cl A
by PRE_TOPC:def 7;
hence
x in [:(Cl A),(Cl B):]
by A3, A7, ZFMISC_1:87;
verum
end;
let x be object ; TARSKI:def 3 ( not x in [:(Cl A),(Cl B):] or x in Cl [:A,B:] )
assume
x in [:(Cl A),(Cl B):]
; x in Cl [:A,B:]
then consider x1, x2 being object such that
A11:
x1 in Cl A
and
A12:
x2 in Cl B
and
A13:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider S1 = S, T1 = T as non empty TopSpace by A11, A12;
reconsider x1 = x1 as Point of S1 by A11;
consider K1 being Basis of x1 such that
A14:
for Q being Subset of S1 st Q in K1 holds
A meets Q
by A11, YELLOW13:17;
reconsider x2 = x2 as Point of T1 by A12;
consider K2 being Basis of x2 such that
A15:
for Q being Subset of T1 st Q in K2 holds
B meets Q
by A12, YELLOW13:17;
for G being Subset of [:S1,T1:] st G is open & [x1,x2] in G holds
[:A,B:] meets G
proof
let G be
Subset of
[:S1,T1:];
( G is open & [x1,x2] in G implies [:A,B:] meets G )
assume that A16:
G is
open
and A17:
[x1,x2] in G
;
[:A,B:] meets G
consider F being
Subset-Family of
[:S1,T1:] such that A18:
G = union F
and A19:
for
e being
set st
e in F holds
ex
X1 being
Subset of
S1 ex
Y1 being
Subset of
T1 st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A16, BORSUK_1:5;
consider Z being
set such that A20:
[x1,x2] in Z
and A21:
Z in F
by A17, A18, TARSKI:def 4;
consider X1 being
Subset of
S1,
Y1 being
Subset of
T1 such that A22:
Z = [:X1,Y1:]
and A23:
X1 is
open
and A24:
Y1 is
open
by A19, A21;
x2 in Y1
by A20, A22, ZFMISC_1:87;
then consider V2 being
Subset of
T1 such that A25:
V2 in K2
and A26:
V2 c= Y1
by A24, YELLOW_8:def 1;
B meets V2
by A15, A25;
then consider a2 being
object such that A27:
a2 in B
and A28:
a2 in V2
by XBOOLE_0:3;
x1 in X1
by A20, A22, ZFMISC_1:87;
then consider V1 being
Subset of
S1 such that A29:
V1 in K1
and A30:
V1 c= X1
by A23, YELLOW_8:def 1;
A meets V1
by A14, A29;
then consider a1 being
object such that A31:
a1 in A
and A32:
a1 in V1
by XBOOLE_0:3;
[a1,a2] in Z
by A22, A30, A32, A26, A28, ZFMISC_1:87;
then A33:
[a1,a2] in union F
by A21, TARSKI:def 4;
[a1,a2] in [:A,B:]
by A31, A27, ZFMISC_1:87;
hence
[:A,B:] meets G
by A18, A33, XBOOLE_0:3;
verum
end;
hence
x in Cl [:A,B:]
by A13, PRE_TOPC:def 7; verum