theorem :: SETLIM_1:55

for X being set
for B being SetSequence of X holds lim_inf B = lim (inferior_setsequence B) by Th43;