for X, Y being TopSpace
for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )