let X be set ; :: thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) )
assume A0: ( B is constant & the_value_of B = A ) ; :: thesis: ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
then B: for n being Element of NAT holds (inferior_setsequence B) . n = A by Th125;
A2: for n being Element of NAT holds (superior_setsequence B) . n = A by A0, Th126;
A3: lim_inf B = A by B, Th185;
lim_sup B = A by A2, Th186;
hence ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) by A3, KURATO_2:def 7; :: thesis: verum