:: deftheorem Def2 defines lim-inf WAYBEL33:def 2 :
for L being non empty TopRelStr holds
( L is lim-inf iff the topology of L = xi L );