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 that
A1: union B1 = the carrier of T1 and
A2: 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;
A3: 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
A4: x = [:a,b:] and
A5: a in B1 and
A6: b in B2 ;
A7: B1 c= the topology of T1 by TOPS_2:78;
A8: B2 c= the topology of T2 by TOPS_2:78;
A9: a is open by A5, A7, PRE_TOPC:def 5;
b is open by A6, A8, PRE_TOPC:def 5;
then [:a,b:] is open by A9, BORSUK_1:46;
hence x in the topology of [:T1,T2:] by A4, PRE_TOPC:def 5; :: thesis: verum

end;

then UniCl CC c= UniCl the topology of [:T1,T2:] by CANTOR_1:9;
then A10: 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 A11: 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 A11, 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
A12: x = [:the carrier of T1,b:] and
A13: 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:] ;
A14: 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 A13; :: 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
A15: p1 in the carrier of T1 and
A16: p2 in b and
A17: [p1,p2] = z by A12, ZFMISC_1:def 2;
consider a being set such that
A18: p1 in a and
A19: a in B1 by A1, A15, TARSKI:def 4;
reconsider a = a as Subset of T1 by A19;
A20: [:a,b:] in Y by A19;
z in [:a,b:] by A16, A17, A18, ZFMISC_1:def 2;
hence z in union Y by A20, 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
A21: z in y and
A22: y in Y by TARSKI:def 4;
ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) by A22;
then y c= x by A12, ZFMISC_1:118;
hence z in x by A21; :: thesis: verum

end;

hence x in UniCl CC by A14, 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
A23: x = [:a,the carrier of T2:] and
A24: 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:] ;
A25: 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 A24; :: 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
A26: p1 in a and
A27: p2 in the carrier of T2 and
A28: [p1,p2] = z by A23, ZFMISC_1:def 2;
consider b being set such that
A29: p2 in b and
A30: b in B2 by A2, A27, TARSKI:def 4;
reconsider b = b as Subset of T2 by A30;
A31: [:a,b:] in Y by A30;
z in [:a,b:] by A26, A28, A29, ZFMISC_1:def 2;
hence z in union Y by A31, 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
A32: z in y and
A33: y in Y by TARSKI:def 4;
ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) by A33;
then y c= x by A23, ZFMISC_1:118;
hence z in x by A32; :: thesis: verum

end;

hence x in UniCl CC by A25, 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 A3, A10, CANTOR_1:def 5, TOPS_2:78;
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