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 5;
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 3;
A2: [a,b] in Int H by CONNSP_2:def 1;
consider F being Subset-Family of [:T,T:] such that
A3: Int H = union F and
A4: 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:45;
consider M being set such that
A5: ( [a,b] in M & M in F ) by A2, A3, TARSKI:def 4;
consider A, B being Subset of T such that
A6: ( M = [:A,B:] & A is open & B is open ) by A4, A5;
( a in A & b in B ) by A5, A6, ZFMISC_1:106;
then A7: ( a in Int A & b in Int B ) by A6, TOPS_1:55;
then reconsider A = A as open a_neighborhood of a by A6, CONNSP_2:def 1;
reconsider B = B as open a_neighborhood of b by A6, A7, 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 set ; :: 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
A9: ( x = g * h & g in A & h in B ) ;
[g,h] in M by A6, A9, ZFMISC_1:106;
then A10: [g,h] in Int H by A3, A5, TARSKI:def 4;
Int H c= H by TOPS_1:44;
then x in f .: H by A9, A10, FUNCT_2:43;
hence x in W by A1; :: thesis: verum