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 & B2 c= the topology of T2 )
by CANTOR_1:def 2;
BB is Basis of [:T1,T2:]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the topology of [:T1,T2:] or x in UniCl BB )
assume A4:
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 A4, PRE_TOPC:def 5;
then A5:
X = union (Base-Appr X)
by BORSUK_1:54;
set Y =
BB /\ (Base-Appr X);
A6:
(
BB /\ (Base-Appr X) c= BB &
BB /\ (Base-Appr X) c= Base-Appr X )
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 A5, 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 A7:
z in X
;
:: thesis: z in union Y
then reconsider p =
z as
Point of
[:T1,T2:] ;
consider z1,
z2 being
set such that A8:
(
z1 in the
carrier of
T1 &
z2 in the
carrier of
T2 &
p = [z1,z2] )
by A1, ZFMISC_1:def 2;
reconsider z1 =
z1 as
Point of
T1 by A8;
reconsider z2 =
z2 as
Point of
T2 by A8;
consider Z being
set such that A9:
(
z in Z &
Z in Base-Appr X )
by A5, A7, TARSKI:def 4;
A10:
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 A11:
(
Z = [:a,b:] &
[:a,b:] c= X &
a is
open &
b is
open )
by A9;
A12:
(
z1 in a &
z2 in b )
by A8, A9, A11, ZFMISC_1:106;
then consider a' being
Subset of
T1 such that A13:
(
a' in B1 &
z1 in a' &
a' c= a )
by A11, Th31;
consider b' being
Subset of
T2 such that A14:
(
b' in B2 &
z2 in b' &
b' c= b )
by A11, A12, Th31;
[:a',b':] c= [:a,b:]
by A13, A14, ZFMISC_1:119;
then
(
[:a',b':] c= X &
a' is
open &
b' is
open )
by A2, A11, A13, A14, PRE_TOPC:def 5, XBOOLE_1:1;
then
(
[:a',b':] in Base-Appr X &
[:a',b':] in BB )
by A10, A13, A14;
then
(
p in [:a',b':] &
[:a',b':] in Y )
by A8, A13, A14, XBOOLE_0:def 4, ZFMISC_1:106;
hence
z in union Y
by TARSKI:def 4;
:: thesis: verum
end;
hence
x in UniCl BB
by A6, 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