let T1, T2 be non empty TopSpace; 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; 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; { [: 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
by PRE_TOPC:def 1;
A2:
cT2 in the topology of T2
by PRE_TOPC:def 1;
A3:
B1 c= the topology of T1
by TOPS_2:64;
A4:
B2 c= the topology of T2
by TOPS_2:64;
{ [: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
A5:
C is
open
proof
let x be
Subset of
[:T1,T2:];
TOPS_2:def 1 ( not x in C or x is open )
assume
x in C
;
x is open
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 A6:
x = [:a,b:]
and A7:
a in the
topology of
T1
and A8:
b in the
topology of
T2
by A1, A2, A3, A4;
A9:
a is
open
by A7;
b is
open
by A8;
hence
x is
open
by A6, A9, BORSUK_1:6;
verum
end;
C is
quasi_prebasis
proof
take
D
;
CANTOR_1:def 4 D c= FinMeetCl C
let d be
object ;
TARSKI:def 3 ( not d in D or d in FinMeetCl C )
assume
d in D
;
d in FinMeetCl C
then consider a being
Subset of
T1,
b being
Subset of
T2 such that A10:
d = [:a,b:]
and A11:
a in D1
and A12:
b in D2
;
consider aY being
Subset-Family of
T1 such that A13:
aY c= B1
and A14:
aY is
finite
and A15:
a = Intersect aY
by A11, CANTOR_1:def 3;
consider bY being
Subset-Family of
T2 such that A16:
bY c= B2
and A17:
bY is
finite
and A18:
b = Intersect bY
by A12, CANTOR_1:def 3;
deffunc H1(
Subset of
T1)
-> Element of
bool the
carrier of
[:T1,T2:] =
[:$1,cT2:];
A19:
{ H1(s) where s is Subset of T1 : s in aY } is
finite
from FRAENKEL:sch 21(A14);
deffunc H2(
Subset of
T2)
-> Element of
bool the
carrier of
[:T1,T2:] =
[:cT1,$1:];
A20:
{ H2(s) where s is Subset of T2 : s in bY } is
finite
from FRAENKEL:sch 21(A17);
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 } ;
A21:
{ [:s,cT2:] where s is Subset of T1 : s in aY } c= C
A22:
{ [: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 } ;
A23:
{ [: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 A21, A22, 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;
Intersect Y = [:a,b:]
hence
d in FinMeetCl C
by A19, A20, A23, CANTOR_1:def 3, A10;
verum
end;
hence
C is
prebasis of
[:T1,T2:]
by A5;
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:]
; verum