let T1, T2 be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: { [: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:] ;
reconsider BB = BB as Subset-Family of [:T1,T2:] ;
A2:
B1 c= the topology of T1
by CANTOR_1:def 2;
A3:
B2 c= the topology of T2
by CANTOR_1:def 2;
BB is Basis of [:T1,T2:]
proof
hereby :: according to TARSKI:def 3,
CANTOR_1:def 2 :: thesis: the topology of [:T1,T2:] c= UniCl BB
let x be
set ;
:: thesis: ( x in BB implies x in the topology of [:T1,T2:] )assume
x in BB
;
:: thesis: x in the topology of [:T1,T2:]then consider a being
Subset of
T1,
b being
Subset of
T2 such that A4:
x = [:a,b:]
and A5:
a in B1
and A6:
b in B2
;
A7:
a is
open
by A2, A5, PRE_TOPC:def 5;
b is
open
by A3, A6, PRE_TOPC:def 5;
then
[:a,b:] is
open
by A7, BORSUK_1:46;
hence
x in the
topology of
[:T1,T2:]
by A4, PRE_TOPC:def 5;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the topology of [:T1,T2:] or x in UniCl BB )
assume A8:
x in the
topology of
[:T1,T2:]
;
:: thesis: 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;
:: according to XBOOLE_0:def 10 :: thesis: X c= union Y
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in X or z in union Y )
assume A11:
z in X
;
:: thesis: 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 a' being
Subset of
T1 such that A24:
a' in B1
and A25:
z1 in a'
and A26:
a' c= a
by A20, A22, Th31;
consider b' being
Subset of
T2 such that A27:
b' in B2
and A28:
z2 in b'
and A29:
b' c= b
by A21, A23, Th31;
[:a',b':] c= [:a,b:]
by A26, A29, ZFMISC_1:119;
then A30:
[:a',b':] c= X
by A19, XBOOLE_1:1;
A31:
a' is
open
by A2, A24, PRE_TOPC:def 5;
b' is
open
by A3, A27, PRE_TOPC:def 5;
then A32:
[:a',b':] in Base-Appr X
by A17, A30, A31;
A33:
[:a',b':] in BB
by A24, A27;
A34:
p in [:a',b':]
by A14, A25, A28, ZFMISC_1:106;
[:a',b':] in Y
by A32, A33, XBOOLE_0:def 4;
hence
z in union Y
by A34, TARSKI:def 4;
:: thesis: verum
end;
hence
x in UniCl BB
by A10, CANTOR_1:def 1;
:: thesis: 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:]
; :: thesis: verum