take lim_sup S ; :: thesis: ( lim_sup S = lim_sup S & lim_sup S = lim_inf S )
thus ( lim_sup S = lim_sup S & lim_sup S = lim_inf S ) by Def7; :: thesis: verum