let T be 1 -element TopSpace-like TopRelStr ; ( T is reflexive implies T is topological_semilattice )
assume
T is reflexive
; T is topological_semilattice
then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ;
consider d being Element of W such that
A1:
the carrier of W = {d}
by TEX_1:def 1;
let f be Function of [:T,T:],T; YELLOW13:def 5 ( f = inf_op T implies f is continuous )
assume A2:
f = inf_op T
; f is continuous
now for P1 being Subset of T st P1 is closed holds
f " P1 is closed let P1 be
Subset of
T;
( P1 is closed implies f " b1 is closed )assume
P1 is
closed
;
f " b1 is closed per cases
( P1 = {} or P1 = the carrier of W )
by TDLAT_3:19;
suppose A3:
P1 = the
carrier of
W
;
f " b1 is closed A4:
dom f =
the
carrier of
[:T,T:]
by FUNCT_2:def 1
.=
[: the carrier of T, the carrier of T:]
by BORSUK_1:def 2
;
A5:
f " P1 = [:{d},{d}:]
proof
thus
for
x being
object st
x in f " P1 holds
x in [:{d},{d}:]
by A1, A4, FUNCT_1:def 7;
TARSKI:def 3,
XBOOLE_0:def 10 [:{d},{d}:] c= f " P1
let x be
object ;
TARSKI:def 3 ( not x in [:{d},{d}:] or x in f " P1 )
A6:
[d,d] in [: the carrier of T, the carrier of T:]
by ZFMISC_1:87;
assume
x in [:{d},{d}:]
;
x in f " P1
then
x in {[d,d]}
by ZFMISC_1:29;
then A7:
x = [d,d]
by TARSKI:def 1;
f . (
d,
d) =
d "/\" d
by A2, WAYBEL_2:def 4
.=
d
by YELLOW_0:25
;
hence
x in f " P1
by A3, A4, A7, A6, FUNCT_1:def 7;
verum
end;
[#] [:T,T:] = [:{d},{d}:]
by A1, BORSUK_1:def 2;
hence
f " P1 is
closed
by A5;
verum end; end; end;
hence
f is continuous
; verum