let T be non empty TopSpace-like TopRelStr ; :: thesis: ( T is reflexive & T is trivial implies T is topological_semilattice )
assume ( T is reflexive & T is trivial ) ; :: thesis: T is topological_semilattice
then reconsider W = T as non empty trivial 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

let P1 be Subset of T; :: thesis: ( P1 is closed implies f " b₁ is closed )
assume P1 is closed ; :: thesis: f " b₁ is closed

per cases ( P1 = {} or P1 = the carrier of W ) by TDLAT_3:21;

suppose P1 = {} ; :: thesis: f " b₁ is closed

then f " P1 = {} [:T,T:] by RELAT_1:171;
hence f " P1 is closed ; :: thesis: verum

end;

suppose A3: P1 = the carrier of W ; :: thesis: f " b₁ 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 5 ;
A5: f " P1 = [:{d},{d}:]

proof

thus for x being set st x in f " P1 holds
x in [:{d},{d}:] by A1, A4, FUNCT_1:def 13; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:{d},{d}:] c= f " P1
let x be set ; :: 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:106;
assume x in [:{d},{d}:] ; :: thesis: x in f " P1
then x in {[d,d]} by ZFMISC_1:35;
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 13; :: thesis: verum

end;

[#] [:T,T:] = [:{d},{d}:] by A1, BORSUK_1:def 5;
hence f " P1 is closed by A5; :: thesis: verum

end;

end;

end;

hence f is continuous by PRE_TOPC:def 12; :: thesis: verum