theorem :: YELLOW_9:43

for T1, T2 being non empty TopSpace
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:]