let X be set ; :: thesis: for A being Subset of X
for Si being SigmaField of X
for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let A be Subset of X; :: thesis: for Si being SigmaField of X
for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let S be SetSequence of Si; :: thesis: ( S is constant & the_value_of S = A implies ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) )
A1: for B being SetSequence of X st B is constant & the_value_of B = A holds
( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )

proof

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) )
A2: ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ;
assume ( B is constant & the_value_of B = A ) ; :: thesis: ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )
hence ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) by A2, Th58; :: thesis: verum

end;

assume ( S is constant & the_value_of S = A ) ; :: thesis: ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
then ( lim_inf S = A & lim_sup S = A ) by A1;
hence ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) by KURATO_0:def 5; :: thesis: verum