let a, b be Point of I[01]; :: thesis: 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

let N be a_neighborhood of a * b; :: thesis: 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

set g = I[01]-TIMES ;
I[01]-TIMES . (a,b) = a * b by Th6;
then consider H being a_neighborhood of [a,b] such that
A1: I[01]-TIMES .: H c= N by BORSUK_1:def 1;
consider F being Subset-Family of such that
A2: Int H = union F and
A3: for e being set st e in F holds
ex X1, Y1 being Subset of I[01] st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
[a,b] in Int H by CONNSP_2:def 1;
then consider M being set such that
A4: [a,b] in M and
A5: M in F by ;
consider A, B being Subset of I[01] such that
A6: M = [:A,B:] and
A7: A is open and
A8: B is open by A3, A5;
a in A by ;
then A9: a in Int A by ;
b in B by ;
then b in Int B by ;
then reconsider B = B as open a_neighborhood of b by ;
reconsider A = A as open a_neighborhood of a by ;
take A ; :: thesis: ex N2 being a_neighborhood of b st
for x, y being Point of I[01] st x in A & y in N2 holds
x * y in N

take B ; :: thesis: for x, y being Point of I[01] st x in A & y in B holds
x * y in N

let x, y be Point of I[01]; :: thesis: ( x in A & y in B implies x * y in N )
assume A10: ( x in A & y in B ) ; :: thesis: x * y in N
A11: Int H c= H by TOPS_1:16;
A12: I[01]-TIMES . (x,y) = x * y by Th6;
[x,y] in M by ;
then [x,y] in Int H by ;
then I[01]-TIMES . (x,y) in I[01]-TIMES .: H by ;
hence x * y in N by ; :: thesis: verum