let T1, T2 be non empty TopSpace; for B1 being Basis of T1
for B2 being Basis of T2 holds { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]
let B1 be Basis of T1; for B2 being Basis of T2 holds { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]
let B2 be Basis of T2; { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]
set BB = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } ;
set T = [:T1,T2:];
A1:
the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:]
by BORSUK_1:def 5;
{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } c= bool the carrier of [:T1,T2:]
then reconsider BB = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } as Subset-Family of [:T1,T2:] ;
A2:
B1 c= the topology of T1
by TOPS_2:78;
A3:
B2 c= the topology of T2
by TOPS_2:78;
BB is Basis of [:T1,T2:]
proof
A90:
BB is
open
BB is
quasi_basis
proof
let x be
set ;
TARSKI:def 3,
CANTOR_1:def 2 ( not x in the topology of [:T1,T2:] or x in UniCl BB )
assume A8:
x in the
topology of
[:T1,T2:]
;
x in UniCl BB
then reconsider X =
x as
Subset of
[:T1,T2:] ;
X is
open
by A8, PRE_TOPC:def 5;
then A9:
X = union (Base-Appr X)
by BORSUK_1:54;
set Y =
BB /\ (Base-Appr X);
A10:
BB /\ (Base-Appr X) c= BB
by XBOOLE_1:17;
reconsider Y =
BB /\ (Base-Appr X) as
Subset-Family of
[:T1,T2:] ;
union Y = X
proof
thus
union Y c= X
by A9, XBOOLE_1:17, ZFMISC_1:95;
XBOOLE_0:def 10 X c= union Y
let z be
set ;
TARSKI:def 3 ( not z in X or z in union Y )
assume A11:
z in X
;
z in union Y
then reconsider p =
z as
Point of
[:T1,T2:] ;
consider z1,
z2 being
set such that A12:
z1 in the
carrier of
T1
and A13:
z2 in the
carrier of
T2
and A14:
p = [z1,z2]
by A1, ZFMISC_1:def 2;
reconsider z1 =
z1 as
Point of
T1 by A12;
reconsider z2 =
z2 as
Point of
T2 by A13;
consider Z being
set such that A15:
z in Z
and A16:
Z in Base-Appr X
by A9, A11, TARSKI:def 4;
A17:
Base-Appr X = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( [:a,b:] c= X & a is open & b is open ) }
by BORSUK_1:def 6;
then consider a being
Subset of
T1,
b being
Subset of
T2 such that A18:
Z = [:a,b:]
and A19:
[:a,b:] c= X
and A20:
a is
open
and A21:
b is
open
by A16;
A22:
z1 in a
by A14, A15, A18, ZFMISC_1:106;
A23:
z2 in b
by A14, A15, A18, ZFMISC_1:106;
consider a9 being
Subset of
T1 such that A24:
a9 in B1
and A25:
z1 in a9
and A26:
a9 c= a
by A20, A22, Th31;
consider b9 being
Subset of
T2 such that A27:
b9 in B2
and A28:
z2 in b9
and A29:
b9 c= b
by A21, A23, Th31;
[:a9,b9:] c= [:a,b:]
by A26, A29, ZFMISC_1:119;
then A30:
[:a9,b9:] c= X
by A19, XBOOLE_1:1;
A31:
a9 is
open
by A2, A24, PRE_TOPC:def 5;
b9 is
open
by A3, A27, PRE_TOPC:def 5;
then A32:
[:a9,b9:] in Base-Appr X
by A17, A30, A31;
A33:
[:a9,b9:] in BB
by A24, A27;
A34:
p in [:a9,b9:]
by A14, A25, A28, ZFMISC_1:106;
[:a9,b9:] in Y
by A32, A33, XBOOLE_0:def 4;
hence
z in union Y
by A34, TARSKI:def 4;
verum
end;
hence
x in UniCl BB
by A10, CANTOR_1:def 1;
verum
end;
hence
BB is
Basis of
[:T1,T2:]
by A90;
verum
end;
hence
{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]
; verum