let T1, T2 be non empty TopSpace; :: thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 holds { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]
set T = [:T1,T2:];
let B1 be prebasis of T1; :: thesis: for B2 being prebasis of T2 holds { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]
let B2 be prebasis of T2; :: thesis: { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]
set C2 = { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } ;
set C1 = { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } ;
reconsider D1 = FinMeetCl B1 as Basis of T1 by Th23;
reconsider D2 = FinMeetCl B2 as Basis of T2 by Th23;
reconsider D = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in D1 & b in D2 ) } as Basis of [:T1,T2:] by Th40;
the carrier of T1 c= the carrier of T1
;
then reconsider cT1 = the carrier of T1 as Subset of T1 ;
the carrier of T2 c= the carrier of T2
;
then reconsider cT2 = the carrier of T2 as Subset of T2 ;
A1:
( cT1 in the topology of T1 & cT2 in the topology of T2 )
by PRE_TOPC:def 1;
A2:
( B1 c= the topology of T1 & B2 c= the topology of T2 )
by CANTOR_1:def 5;
{ [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } c= bool the carrier of [:T1,T2:]
then reconsider C1 = { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } as Subset-Family of [:T1,T2:] ;
reconsider C1 = C1 as Subset-Family of [:T1,T2:] ;
{ [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } c= bool the carrier of [:T1,T2:]
then reconsider C2 = { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } as Subset-Family of [:T1,T2:] ;
reconsider C2 = C2 as Subset-Family of [:T1,T2:] ;
reconsider C = C2 \/ C1 as Subset-Family of [:T1,T2:] ;
C is prebasis of [:T1,T2:]
proof
hereby :: according to TARSKI:def 3,
CANTOR_1:def 5 :: thesis: ex b1 being Basis of [:T1,T2:] st b1 c= FinMeetCl C
let x be
set ;
:: thesis: ( x in C implies x in the topology of [:T1,T2:] )assume
x in C
;
:: thesis: x in the topology of [:T1,T2:]then
(
x in C1 or
x in C2 )
by XBOOLE_0:def 3;
then
( ex
a being
Subset of
T1 st
(
x = [:a,cT2:] &
a in B1 ) or ex
a being
Subset of
T2 st
(
x = [:cT1,a:] &
a in B2 ) )
;
then consider a being
Subset of
T1,
b being
Subset of
T2 such that A3:
(
x = [:a,b:] &
a in the
topology of
T1 &
b in the
topology of
T2 )
by A1, A2;
(
a is
open &
b is
open )
by A3, PRE_TOPC:def 5;
then
[:a,b:] is
open
by BORSUK_1:46;
hence
x in the
topology of
[:T1,T2:]
by A3, PRE_TOPC:def 5;
:: thesis: verum
end;
take
D
;
:: thesis: D c= FinMeetCl C
let d be
set ;
:: according to TARSKI:def 3 :: thesis: ( not d in D or d in FinMeetCl C )
assume
d in D
;
:: thesis: d in FinMeetCl C
then consider a being
Subset of
T1,
b being
Subset of
T2 such that A4:
(
d = [:a,b:] &
a in D1 &
b in D2 )
;
consider aY being
Subset-Family of
T1 such that A5:
aY c= B1
and A6:
aY is
finite
and A7:
a = Intersect aY
by A4, CANTOR_1:def 4;
consider bY being
Subset-Family of
T2 such that A8:
bY c= B2
and A9:
bY is
finite
and A10:
b = Intersect bY
by A4, CANTOR_1:def 4;
deffunc H1(
Subset of
T1)
-> Element of
bool the
carrier of
[:T1,T2:] =
[:$1,cT2:];
A11:
{ H1(s) where s is Subset of T1 : s in aY } is
finite
from FRAENKEL:sch 21(A6);
deffunc H2(
Subset of
T2)
-> Element of
bool the
carrier of
[:T1,T2:] =
[:cT1,$1:];
A12:
{ H2(s) where s is Subset of T2 : s in bY } is
finite
from FRAENKEL:sch 21(A9);
set Y1 =
{ [:s,cT2:] where s is Subset of T1 : s in aY } ;
set Y2 =
{ [:cT1,s:] where s is Subset of T2 : s in bY } ;
A13:
{ [:s,cT2:] where s is Subset of T1 : s in aY } c= C
A15:
{ [:cT1,s:] where s is Subset of T2 : s in bY } c= C
set Y =
{ [:s,cT2:] where s is Subset of T1 : s in aY } \/ { [:cT1,s:] where s is Subset of T2 : s in bY } ;
A17:
{ [:s,cT2:] where s is Subset of T1 : s in aY } \/ { [:cT1,s:] where s is Subset of T2 : s in bY } c= C
by A13, A15, XBOOLE_1:8;
then reconsider Y =
{ [:s,cT2:] where s is Subset of T1 : s in aY } \/ { [:cT1,s:] where s is Subset of T2 : s in bY } as
Subset-Family of
[:T1,T2:] by XBOOLE_1:1;
A18:
Y is
finite
by A11, A12;
Intersect Y = d
hence
d in FinMeetCl C
by A17, A18, CANTOR_1:def 4;
:: thesis: verum
end;
hence
{ [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]
; :: thesis: verum