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 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:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:a, the carrier of T2:] where a is Subset of T1 : a in B1 } or x in bool the carrier of [:T1,T2:] )
assume x in { [:a, the carrier of T2:] where a is Subset of T1 : a in B1 } ; :: thesis: x in bool the carrier of [:T1,T2:]
then ex a being Subset of T1 st
( x = [:a,cT2:] & a in B1 ) ;
hence x in bool the carrier of [:T1,T2:] ; :: thesis: verum
end;
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:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [: the carrier of T1,b:] where b is Subset of T2 : b in B2 } or x in bool the carrier of [:T1,T2:] )
assume x in { [: the carrier of T1,b:] where b is Subset of T2 : b in B2 } ; :: thesis: x in bool the carrier of [:T1,T2:]
then ex a being Subset of T2 st
( x = [:cT1,a:] & a in B2 ) ;
hence x in bool the carrier of [:T1,T2:] ; :: thesis: verum
end;
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:]; :: according to TOPS_2:def 1 :: thesis: ( not x in C or x is open )
assume x in C ; :: thesis: 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; :: thesis: verum
end;
C is quasi_prebasis
proof
take D ; :: according to CANTOR_1:def 4 :: thesis: D c= FinMeetCl C
let d be object ; :: 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
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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:s,cT2:] where s is Subset of T1 : s in aY } or x in C )
assume x in { [:s,cT2:] where s is Subset of T1 : s in aY } ; :: thesis: x in C
then ex s being Subset of T1 st
( x = [:s,cT2:] & s in aY ) ;
then x in C1 by A13;
hence x in C by XBOOLE_0:def 3; :: thesis: verum
end;
A22: { [:cT1,s:] where s is Subset of T2 : s in bY } c= C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:cT1,s:] where s is Subset of T2 : s in bY } or x in C )
assume x in { [:cT1,s:] where s is Subset of T2 : s in bY } ; :: thesis: x in C
then ex s being Subset of T2 st
( x = [:cT1,s:] & s in bY ) ;
then x in C2 by A16;
hence x in C by XBOOLE_0:def 3; :: thesis: verum
end;
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:]
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:a,b:] c= Intersect Y
let p be object ; :: thesis: ( p in Intersect Y implies p in [:a,b:] )
assume A24: p in Intersect Y ; :: thesis: p in [:a,b:]
then consider p1 being Point of T1, p2 being Point of T2 such that
A25: p = [p1,p2] by BORSUK_1:10;
now :: thesis: for z being set st z in aY holds
p1 in z
let z be set ; :: thesis: ( z in aY implies p1 in z )
assume A26: z in aY ; :: thesis: p1 in z
then reconsider z9 = z as Subset of T1 ;
[:z9,cT2:] in { [:s,cT2:] where s is Subset of T1 : s in aY } by A26;
then [:z9,cT2:] in Y by XBOOLE_0:def 3;
then p in [:z9,cT2:] by A24, SETFAM_1:43;
hence p1 in z by A25, ZFMISC_1:87; :: thesis: verum
end;
then A27: p1 in a by A15, SETFAM_1:43;
now :: thesis: for z being set st z in bY holds
p2 in z
let z be set ; :: thesis: ( z in bY implies p2 in z )
assume A28: z in bY ; :: thesis: p2 in z
then reconsider z9 = z as Subset of T2 ;
[:cT1,z9:] in { [:cT1,s:] where s is Subset of T2 : s in bY } by A28;
then [:cT1,z9:] in Y by XBOOLE_0:def 3;
then p in [:cT1,z9:] by A24, SETFAM_1:43;
hence p2 in z by A25, ZFMISC_1:87; :: thesis: verum
end;
then p2 in b by A18, SETFAM_1:43;
hence p in [:a,b:] by A25, A27, ZFMISC_1:87; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in [:a,b:] or p in Intersect Y )
assume p in [:a,b:] ; :: thesis: p in Intersect Y
then consider p1, p2 being object such that
A29: p1 in a and
A30: p2 in b and
A31: [p1,p2] = p by ZFMISC_1:def 2;
reconsider p1 = p1 as Point of T1 by A29;
reconsider p2 = p2 as Point of T2 by A30;
now :: thesis: for z being set st z in Y holds
[p1,p2] in z
let z be set ; :: thesis: ( z in Y implies [p1,p2] in b1 )
assume A32: z in Y ; :: thesis: [p1,p2] in b1
per cases ( z in { [:s,cT2:] where s is Subset of T1 : s in aY } or z in { [:cT1,s:] where s is Subset of T2 : s in bY } ) by A32, XBOOLE_0:def 3;
suppose z in { [:s,cT2:] where s is Subset of T1 : s in aY } ; :: thesis: [p1,p2] in b1
then consider s being Subset of T1 such that
A33: z = [:s,cT2:] and
A34: s in aY ;
p1 in s by A15, A29, A34, SETFAM_1:43;
hence [p1,p2] in z by A33, ZFMISC_1:87; :: thesis: verum
end;
suppose z in { [:cT1,s:] where s is Subset of T2 : s in bY } ; :: thesis: [p1,p2] in b1
then consider s being Subset of T2 such that
A35: z = [:cT1,s:] and
A36: s in bY ;
p2 in s by A18, A30, A36, SETFAM_1:43;
hence [p1,p2] in z by A35, ZFMISC_1:87; :: thesis: verum
end;
end;
end;
hence p in Intersect Y by A31, SETFAM_1:43; :: thesis: verum
end;
hence d in FinMeetCl C by A19, A20, A23, CANTOR_1:def 3, A10; :: thesis: verum
end;
hence C is prebasis of [:T1,T2:] by A5; :: 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