let seq be ExtREAL_sequence; :: thesis: ( seq is convergent implies ( lim seq = lim_inf seq & lim seq = lim_sup seq ) )

set a = lim_inf seq;

assume seq is convergent ; :: thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )

then A1: lim_inf seq = lim_sup seq by Th40;

set a = lim_inf seq;

assume seq is convergent ; :: thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )

then A1: lim_inf seq = lim_sup seq by Th40;