let S, T be TopSpace; :: thesis: 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; :: thesis: for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

let B be Subset of T; :: thesis: Cl [:A,B:] = [:(Cl A),(Cl B):]

assume x in [:(Cl A),(Cl B):] ; :: thesis: 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

for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

let A be Subset of S; :: thesis: for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

let B be Subset of T; :: thesis: Cl [:A,B:] = [:(Cl A),(Cl B):]

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:(Cl A),(Cl B):] c= Cl [:A,B:]

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Cl A),(Cl B):] or x in Cl [:A,B:] )let x be object ; :: thesis: ( x in Cl [:A,B:] implies x in [:(Cl A),(Cl B):] )

assume A1: x in Cl [:A,B:] ; :: thesis: 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

for G being Subset of S1 st G is open & p1 in G holds

A meets G

hence x in [:(Cl A),(Cl B):] by A3, A7, ZFMISC_1:87; :: thesis: verum

end;assume A1: x in Cl [:A,B:] ; :: thesis: 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

then A7:
p2 in Cl B
by PRE_TOPC:def 7;
let G be Subset of T1; :: thesis: ( G is open & p2 in G implies B meets G )

assume ( G is open & p2 in G ) ; :: thesis: 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 ; :: thesis: verum

end;assume ( G is open & p2 in G ) ; :: thesis: 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 ; :: thesis: verum

for G being Subset of S1 st G is open & p1 in G holds

A meets G

proof

then
p1 in Cl A
by PRE_TOPC:def 7;
let G be Subset of S1; :: thesis: ( G is open & p1 in G implies A meets G )

assume ( G is open & p1 in G ) ; :: thesis: 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 ; :: thesis: verum

end;assume ( G is open & p1 in G ) ; :: thesis: 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 ; :: thesis: verum

hence x in [:(Cl A),(Cl B):] by A3, A7, ZFMISC_1:87; :: thesis: verum

assume x in [:(Cl A),(Cl B):] ; :: thesis: 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

hence
x in Cl [:A,B:]
by A13, PRE_TOPC:def 7; :: thesis: verum
let G be Subset of [:S1,T1:]; :: thesis: ( G is open & [x1,x2] in G implies [:A,B:] meets G )

assume that

A16: G is open and

A17: [x1,x2] in G ; :: thesis: [: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; :: thesis: verum

end;assume that

A16: G is open and

A17: [x1,x2] in G ; :: thesis: [: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; :: thesis: verum