let T1, T2 be non empty TopSpace; :: thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:]
let B1 be prebasis of T1; :: thesis: for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:]
let B2 be prebasis of T2; :: thesis: ( union B1 = the carrier of T1 & union B2 = the carrier of T2 implies { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:] )
assume A1: ( union B1 = the carrier of T1 & union B2 = the carrier of T2 ) ; :: thesis: { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:]
set cT1 = the carrier of T1;
set cT2 = the carrier of T2;
set BB1 = { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } ;
set BB2 = { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } ;
set CC = { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } ;
set T = [:T1,T2:];
reconsider BB = { [: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 } as prebasis of [:T1,T2:] by Th41;
A2: FinMeetCl BB is Basis of [:T1,T2:] by Th23;
{ [: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:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } or x in bool the carrier of [:T1,T2:] )
assume x in { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } ; :: thesis: x in bool the carrier of [:T1,T2:]
then ex a being Subset of T1 ex b being Subset of T2 st
( x = [:a,b:] & a in B1 & b in B2 ) ;
hence x in bool the carrier of [:T1,T2:] ; :: thesis: verum

end;

then reconsider CC = { [: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 CC = CC as Subset-Family of [:T1,T2:] ;
CC c= the topology of [:T1,T2:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in CC or x in the topology of [:T1,T2:] )
assume x in CC ; :: thesis: x in the topology of [:T1,T2:]
then consider a being Subset of T1, b being Subset of T2 such that
A3: ( x = [:a,b:] & a in B1 & b in B2 ) ;
( B1 c= the topology of T1 & B2 c= the topology of T2 ) by CANTOR_1:def 5;
then ( 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;

then UniCl CC c= UniCl the topology of [:T1,T2:] by CANTOR_1:9;
then A4: UniCl CC c= the topology of [:T1,T2:] by CANTOR_1:6;
BB c= UniCl CC

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in BB or x in UniCl CC )
assume A5: x in BB ; :: thesis: x in UniCl CC

per cases ( x in { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } or x in { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } ) by A5, XBOOLE_0:def 3;

suppose x in { [:the carrier of T1,b:] where b is Subset of T2 : b in B2 } ; :: thesis: x in UniCl CC

then consider b being Subset of T2 such that
A6: ( x = [:the carrier of T1,b:] & b in B2 ) ;
set Y = { [:a,b:] where a is Subset of T1 : a in B1 } ;
{ [:a,b:] where a is Subset of T1 : a in B1 } c= bool the carrier of [:T1,T2:]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { [:a,b:] where a is Subset of T1 : a in B1 } or y in bool the carrier of [:T1,T2:] )
assume y in { [:a,b:] where a is Subset of T1 : a in B1 } ; :: thesis: y in bool the carrier of [:T1,T2:]
then ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) ;
hence y in bool the carrier of [:T1,T2:] ; :: thesis: verum

end;

then reconsider Y = { [:a,b:] where a is Subset of T1 : a in B1 } as Subset-Family of [:T1,T2:] ;
reconsider Y = Y as Subset-Family of [:T1,T2:] ;
A7: Y c= CC

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in CC )
assume y in Y ; :: thesis: y in CC
then ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) ;
hence y in CC by A6; :: thesis: verum

end;

x = union Y

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union Y c= x

let z be set ; :: thesis: ( z in x implies z in union Y )
assume z in x ; :: thesis: z in union Y
then consider p1, p2 being set such that
A8: ( p1 in the carrier of T1 & p2 in b & [p1,p2] = z ) by A6, ZFMISC_1:def 2;
consider a being set such that
A9: ( p1 in a & a in B1 ) by A1, A8, TARSKI:def 4;
reconsider a = a as Subset of T1 by A9;
( [:a,b:] in Y & z in [:a,b:] ) by A8, A9, ZFMISC_1:def 2;
hence z in union Y by TARSKI:def 4; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union Y or z in x )
assume z in union Y ; :: thesis: z in x
then consider y being set such that
A10: ( z in y & y in Y ) by TARSKI:def 4;
ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) by A10;
then y c= x by A6, ZFMISC_1:118;
hence z in x by A10; :: thesis: verum

end;

hence x in UniCl CC by A7, CANTOR_1:def 1; :: thesis: verum

end;

suppose x in { [:a,the carrier of T2:] where a is Subset of T1 : a in B1 } ; :: thesis: x in UniCl CC

then consider a being Subset of T1 such that
A11: ( x = [:a,the carrier of T2:] & a in B1 ) ;
set Y = { [:a,b:] where b is Subset of T2 : b in B2 } ;
{ [:a,b:] where b is Subset of T2 : b in B2 } c= bool the carrier of [:T1,T2:]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { [:a,b:] where b is Subset of T2 : b in B2 } or y in bool the carrier of [:T1,T2:] )
assume y in { [:a,b:] where b is Subset of T2 : b in B2 } ; :: thesis: y in bool the carrier of [:T1,T2:]
then ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) ;
hence y in bool the carrier of [:T1,T2:] ; :: thesis: verum

end;

then reconsider Y = { [:a,b:] where b is Subset of T2 : b in B2 } as Subset-Family of [:T1,T2:] ;
reconsider Y = Y as Subset-Family of [:T1,T2:] ;
A12: Y c= CC

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in CC )
assume y in Y ; :: thesis: y in CC
then ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) ;
hence y in CC by A11; :: thesis: verum

end;

x = union Y

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union Y c= x

let z be set ; :: thesis: ( z in x implies z in union Y )
assume z in x ; :: thesis: z in union Y
then consider p1, p2 being set such that
A13: ( p1 in a & p2 in the carrier of T2 & [p1,p2] = z ) by A11, ZFMISC_1:def 2;
consider b being set such that
A14: ( p2 in b & b in B2 ) by A1, A13, TARSKI:def 4;
reconsider b = b as Subset of T2 by A14;
( [:a,b:] in Y & z in [:a,b:] ) by A13, A14, ZFMISC_1:def 2;
hence z in union Y by TARSKI:def 4; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union Y or z in x )
assume z in union Y ; :: thesis: z in x
then consider y being set such that
A15: ( z in y & y in Y ) by TARSKI:def 4;
ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) by A15;
then y c= x by A11, ZFMISC_1:118;
hence z in x by A15; :: thesis: verum

end;

hence x in UniCl CC by A12, CANTOR_1:def 1; :: thesis: verum

end;

end;

end;

then FinMeetCl BB c= FinMeetCl (UniCl CC) by CANTOR_1:16;
then UniCl CC is prebasis of [:T1,T2:] by A2, A4, CANTOR_1:def 5;
hence { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:] by Th24; :: thesis: verum