let T be non empty TopSpace-like topological_semilattice TopRelStr ; :: thesis: for x being Element of T holds x "/\" is continuous
let x be Element of T; :: thesis: x "/\" is continuous
let p be Point of T; :: according to BORSUK_1:def 3 :: thesis: for b₁ being a_neighborhood of (x "/\" ) . p ex b₂ being a_neighborhood of p st (x "/\" ) .: b₂ c= b₁
let G be a_neighborhood of (x "/\" ) . p; :: thesis: ex b₁ being a_neighborhood of p st (x "/\" ) .: b₁ c= G
set TT = [:T,T:];
A1: the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
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: G is a_neighborhood of x "/\" p by WAYBEL_1:def 18;
reconsider xp = [x,p] as Point of [:T,T:] by A1, YELLOW_3:def 2;
A3: f . xp = f . x,p
.= x "/\" p by WAYBEL_2:def 4 ;
f is continuous by Def5;
then consider H being a_neighborhood of xp such that
A4: f .: H c= G by A2, A3, BORSUK_1:def 3;
consider A being Subset-Family of [:T,T:] such that
A5: Int H = union A and
A6: 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:45;
xp in Int H by CONNSP_2:def 1;
then consider Z being set such that
A7: xp in Z and
A8: Z in A by A5, TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A9: Z = [:X1,Y1:] and
A10: ( X1 is open & Y1 is open ) by A6, A8;
p in Y1 by A7, A9, ZFMISC_1:106;
then reconsider Y1 = Y1 as a_neighborhood of p by A10, CONNSP_2:5;
take Y1 ; :: thesis: (x "/\" ) .: Y1 c= G
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in (x "/\" ) .: Y1 or b in G )
assume b in (x "/\" ) .: Y1 ; :: thesis: b in G
then consider a being set such that
a in dom (x "/\" ) and
A11: a in Y1 and
A12: b = (x "/\" ) . a by FUNCT_1:def 12;
reconsider a = a as Element of T by A11;
A13: b = x "/\" a by A12, WAYBEL_1:def 18
.= f . x,a by WAYBEL_2:def 4 ;
x in X1 by A7, A9, ZFMISC_1:106;
then [x,a] in Z by A9, A11, ZFMISC_1:106;
then A14: [x,a] in Int H by A5, A8, TARSKI:def 4;
A15: Int H c= H by TOPS_1:44;
[x,a] in [:the carrier of T,the carrier of T:] by ZFMISC_1:106;
then [x,a] in dom f by A1, FUNCT_2:def 1;
then b in f .: H by A13, A14, A15, FUNCT_1:def 12;
hence b in G by A4; :: thesis: verum