let T be 1 -element TopSpace-like TopRelStr ; :: thesis: ( T is reflexive implies T is topological_semilattice )
assume T is reflexive ; :: thesis: 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; :: according to YELLOW13:def 5 :: thesis: ( f = inf_op T implies f is continuous )
assume A2: f = inf_op T ; :: thesis: f is continuous
now :: thesis: for P1 being Subset of T st P1 is closed holds
f " P1 is closed
let P1 be Subset of T; :: thesis: ( P1 is closed implies f " b1 is closed )
assume P1 is closed ; :: thesis: f " b1 is closed
per cases ( P1 = {} or P1 = the carrier of W ) by TDLAT_3:19;
suppose P1 = {} ; :: thesis: f " b1 is closed
then f " P1 = {} [:T,T:] ;
hence f " P1 is closed ; :: thesis: verum
end;
suppose A3: P1 = the carrier of W ; :: thesis: 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; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:{d},{d}:] c= f " P1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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}:] ; :: thesis: 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; :: thesis: verum
end;
[#] [:T,T:] = [:{d},{d}:] by A1, BORSUK_1:def 2;
hence f " P1 is closed by A5; :: thesis: verum
end;
end;
end;
hence f is continuous ; :: thesis: verum