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):]
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:(Cl A),(Cl B):] c= 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 ;
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; :: 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 ;
then consider V being Subset of [:S1,T1:] such that
A4: V in K and
A5: V c= [:([#] S1),G:] by ;
[: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 ;
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;
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; :: 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 ;
then consider V being Subset of [:S1,T1:] such that
A8: V in K and
A9: V c= [:G,([#] T1):] by ;
[: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 ;
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;
then p1 in Cl A by PRE_TOPC:def 7;
hence x in [:(Cl A),(Cl B):] by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Cl A),(Cl B):] or x in Cl [:A,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 ;
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 ;
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 ;
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:]; :: 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 ;
consider Z being set such that
A20: [x1,x2] in Z and
A21: Z in F by ;
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 ;
x2 in Y1 by ;
then consider V2 being Subset of T1 such that
A25: V2 in K2 and
A26: V2 c= Y1 by ;
B meets V2 by ;
then consider a2 being object such that
A27: a2 in B and
A28: a2 in V2 by XBOOLE_0:3;
x1 in X1 by ;
then consider V1 being Subset of S1 such that
A29: V1 in K1 and
A30: V1 c= X1 by ;
A meets V1 by ;
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 ;
then A33: [a1,a2] in union F by ;
[a1,a2] in [:A,B:] by ;
hence [:A,B:] meets G by ; :: thesis: verum
end;
hence x in Cl [:A,B:] by ; :: thesis: verum