let T be non empty TopSpace-like BinContinuous TopGrStr ; 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; 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; 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
; ex B being open a_neighborhood of b st A * B c= W
take
B
; A * B c= W
let x be object ; TARSKI:def 3 ( not x in A * B or x in W )
assume
x in A * B
; 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; verum