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 2;
{ [: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:64;
A3:
B2 c= the topology of T2
by TOPS_2:64;
BB is Basis of [:T1,T2:]
proof
A4:
BB is
open
BB is
quasi_basis
proof
let x be
object ;
TARSKI:def 3,
CANTOR_1:def 2 ( not x in the topology of [:T1,T2:] or x in UniCl BB )
assume A9:
x in the
topology of
[:T1,T2:]
;
x in UniCl BB
then reconsider X =
x as
Subset of
[:T1,T2:] ;
X is
open
by A9;
then A10:
X = union (Base-Appr X)
by BORSUK_1:13;
set Y =
BB /\ (Base-Appr X);
A11:
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 A10, XBOOLE_1:17, ZFMISC_1:77;
XBOOLE_0:def 10 X c= union Y
let z be
object ;
TARSKI:def 3 ( not z in X or z in union Y )
assume A12:
z in X
;
z in union Y
then reconsider p =
z as
Point of
[:T1,T2:] ;
consider z1,
z2 being
object such that A13:
z1 in the
carrier of
T1
and A14:
z2 in the
carrier of
T2
and A15:
p = [z1,z2]
by A1, ZFMISC_1:def 2;
reconsider z1 =
z1 as
Point of
T1 by A13;
reconsider z2 =
z2 as
Point of
T2 by A14;
consider Z being
set such that A16:
z in Z
and A17:
Z in Base-Appr X
by A10, A12, TARSKI:def 4;
A18:
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 3;
then consider a being
Subset of
T1,
b being
Subset of
T2 such that A19:
Z = [:a,b:]
and A20:
[:a,b:] c= X
and A21:
a is
open
and A22:
b is
open
by A17;
A23:
z1 in a
by A15, A16, A19, ZFMISC_1:87;
A24:
z2 in b
by A15, A16, A19, ZFMISC_1:87;
consider a9 being
Subset of
T1 such that A25:
a9 in B1
and A26:
z1 in a9
and A27:
a9 c= a
by A21, A23, Th31;
consider b9 being
Subset of
T2 such that A28:
b9 in B2
and A29:
z2 in b9
and A30:
b9 c= b
by A22, A24, Th31;
[:a9,b9:] c= [:a,b:]
by A27, A30, ZFMISC_1:96;
then A31:
[:a9,b9:] c= X
by A20;
A32:
a9 is
open
by A2, A25;
b9 is
open
by A3, A28;
then A33:
[:a9,b9:] in Base-Appr X
by A18, A31, A32;
A34:
[:a9,b9:] in BB
by A25, A28;
A35:
p in [:a9,b9:]
by A15, A26, A29, ZFMISC_1:87;
[:a9,b9:] in Y
by A33, A34, XBOOLE_0:def 4;
hence
z in union Y
by A35, TARSKI:def 4;
verum
end;
hence
x in UniCl BB
by A11, CANTOR_1:def 1;
verum
end;
hence
BB is
Basis of
[:T1,T2:]
by A4;
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