theorem Th7: :: TOPALG_7:7

for a, b being Point of I[01]
for N being a_neighborhood of a * b ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st
for x, y being Point of I[01] st x in N1 & y in N2 holds
x * y in N