theorem Th4: :: JCT_MISC:4

for S, T being non empty TopSpace
for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open