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