let T be non empty TopSpace-like BinContinuous TopGrStr ; :: thesis: for a, b being Element of T
for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
let a, b be Element of T; :: thesis: for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
let W be a_neighborhood of a * b; :: thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then reconsider f = the multF of T as Function of [:T,T:],T ;
f is continuous by Def8;
then consider H being a_neighborhood of [a,b] such that
A1: f .: H c= W by BORSUK_1:def 1;
consider F being Subset-Family of [:T,T:] such that
A2: Int H = union F and
A3: for e being set st e in F holds
ex X1, Y1 being Subset of T 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 T 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 B being open a_neighborhood of b st A * B c= W
take B ; :: thesis: A * B c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * B or x in W )
assume x in A * B ; :: thesis: x in W
then consider g, h being Element of T such that
A10: x = g * h and
A11: ( g in A & h in B ) ;
A12: Int H c= H by TOPS_1:16;
[g,h] in M by A6, A11, ZFMISC_1:87;
then [g,h] in Int H by A2, A5, TARSKI:def 4;
then x in f .: H by A10, A12, FUNCT_2:35;
hence x in W by A1; :: thesis: verum