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:]

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

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

( Int V c= V & Int W c= W )
by TOPS_1:16;
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;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

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