let X, Y be TopSpace; 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; for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]
let W be Subset of Y; Int [:V,W:] = [:(Int V),(Int W):]
thus
Int [:V,W:] c= [:(Int V),(Int W):]
XBOOLE_0:def 10 [:(Int V),(Int W):] c= Int [:V,W:]proof
let e be
object ;
TARSKI:def 3 ( not e in Int [:V,W:] or e in [:(Int V),(Int W):] )
assume
e in Int [:V,W:]
;
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;
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; verum