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 [:I[01],I[01]:] 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 A2, TARSKI:def 4;
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 A4, A6, ZFMISC_1:87;
then A9: a in Int A by A7, TOPS_1:23;
b in B by A4, A6, ZFMISC_1:87;
then b in Int B by A8, TOPS_1:23;
then reconsider B = B as open a_neighborhood of b by A8, CONNSP_2:def 1;
reconsider A = A as open a_neighborhood of a by A7, A9, CONNSP_2:def 1;
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 A6, A10, ZFMISC_1:87;
then [x,y] in Int H by A2, A5, TARSKI:def 4;
then I[01]-TIMES . (x,y) in I[01]-TIMES .: H by A11, FUNCT_2:35;
hence x * y in N by A1, A12; :: thesis: verum