:: deftheorem defines lim_inf MESFUN7C:def 6 :
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim_inf f = lim_inf (R_EAL f);