let T be non empty TopSpace-like topological_semilattice TopRelStr ; for x being Element of T holds x "/\" is continuous
let x be Element of T; x "/\" is continuous
let p be Point of T; BORSUK_1:def 1 for b1 being a_neighborhood of (x "/\") . p ex b2 being a_neighborhood of p st (x "/\") .: b2 c= b1
let G be a_neighborhood of (x "/\") . p; ex b1 being a_neighborhood of p st (x "/\") .: b1 c= G
set TT = [:T,T:];
A1:
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:]
by BORSUK_1:def 2;
then reconsider xp = [x,p] as Point of [:T,T:] by YELLOW_3:def 2;
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:]
by YELLOW_3:def 2;
then reconsider f = inf_op T as Function of [:T,T:],T by A1;
A2: f . xp =
f . (x,p)
.=
x "/\" p
by WAYBEL_2:def 4
;
( G is a_neighborhood of x "/\" p & f is continuous )
by Def5, WAYBEL_1:def 18;
then consider H being a_neighborhood of xp such that
A3:
f .: H c= G
by A2;
consider A being Subset-Family of [:T,T:] such that
A4:
Int H = union A
and
A5:
for e being set st e in A holds
ex X1, Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
by BORSUK_1:5;
xp in Int H
by CONNSP_2:def 1;
then consider Z being set such that
A6:
xp in Z
and
A7:
Z in A
by A4, TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A8:
Z = [:X1,Y1:]
and
X1 is open
and
A9:
Y1 is open
by A5, A7;
p in Y1
by A6, A8, ZFMISC_1:87;
then reconsider Y1 = Y1 as a_neighborhood of p by A9, CONNSP_2:3;
take
Y1
; (x "/\") .: Y1 c= G
let b be object ; TARSKI:def 3 ( not b in (x "/\") .: Y1 or b in G )
assume
b in (x "/\") .: Y1
; b in G
then consider a being object such that
a in dom (x "/\")
and
A10:
a in Y1
and
A11:
b = (x "/\") . a
by FUNCT_1:def 6;
reconsider a = a as Element of T by A10;
x in X1
by A6, A8, ZFMISC_1:87;
then
[x,a] in Z
by A8, A10, ZFMISC_1:87;
then A12:
[x,a] in Int H
by A4, A7, TARSKI:def 4;
[x,a] in [: the carrier of T, the carrier of T:]
by ZFMISC_1:87;
then A13:
( Int H c= H & [x,a] in dom f )
by A1, FUNCT_2:def 1, TOPS_1:16;
b =
x "/\" a
by A11, WAYBEL_1:def 18
.=
f . (x,a)
by WAYBEL_2:def 4
;
then
b in f .: H
by A12, A13, FUNCT_1:def 6;
hence
b in G
by A3; verum