:: deftheorem Def3 defines Xi WAYBEL33:def 3 :
for L being up-complete /\-complete Semilattice
for b₂ being strict TopAugmentation of L holds
( b₂ = Xi L iff b₂ is lim-inf );