for T1, T2 being non empty TopSpace
for D being Subset of [:T1,T2:] st D is open holds
for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )