let X, Y be TopSpace; :: thesis: for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let V be Subset of X; :: thesis: for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let W be Subset of Y; :: thesis: Int [:V,W:] = [:(Int V),(Int W):]
thus Int [:V,W:] c= [:(Int V),(Int W):] :: according to XBOOLE_0:def 10 :: thesis: [:(Int V),(Int W):] c= Int [:V,W:]

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Int [:V,W:] or e in [:(Int V),(Int W):] )
assume e in Int [:V,W:] ; :: thesis: e in [:(Int V),(Int W):]
then consider Q being Subset of [:X,Y:] such that
A1: Q is open and
A2: Q c= [:V,W:] and
A3: e in Q by TOPS_1:22;
consider A being Subset-Family of [:X,Y:] such that
A4: Q = union A and
A5: for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A1, Th5;
consider a being set such that
A6: e in a and
A7: a in A by A3, A4, TARSKI:def 4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: a = [:X1,Y1:] and
A9: X1 is open and
A10: Y1 is open by A5, A7;
[:X1,Y1:] c= Q by A4, A7, A8, ZFMISC_1:74;
then A11: [:X1,Y1:] c= [:V,W:] by A2;
then Y1 c= W by A6, A8, ZFMISC_1:114;
then A12: Y1 c= Int W by A10, TOPS_1:24;
X1 c= V by A6, A8, A11, ZFMISC_1:114;
then X1 c= Int V by A9, TOPS_1:24;
then [:X1,Y1:] c= [:(Int V),(Int W):] by A12, ZFMISC_1:96;
hence e in [:(Int V),(Int W):] by A6, A8; :: thesis: verum

end;

( Int V c= V & Int W c= W ) by TOPS_1:16;
then [:(Int V),(Int W):] c= [:V,W:] by ZFMISC_1:96;
hence [:(Int V),(Int W):] c= Int [:V,W:] by Th6, TOPS_1:24; :: thesis: verum