let X be set ; :: thesis: for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B
let A be SetSequence of X; :: thesis: for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B
let B be Subset of X; :: thesis: ( ( for n being Nat holds A . n = B ) implies lim_sup A = B )
assume A1: for n being Nat holds A . n = B ; :: thesis: lim_sup A = B
thus lim_sup A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= lim_sup A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup A or x in B )
assume x in lim_sup A ; :: thesis: x in B
then consider k being Element of NAT such that
A2: x in A . (0 + k) by Th8;
thus x in B by A1, A2; :: thesis: verum

end;

thus B c= lim_sup A :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in lim_sup A )
assume A3: x in B ; :: thesis: x in lim_sup A
for m being Element of NAT ex k being Element of NAT st x in A . (m + k)

proof

let m be Element of NAT ; :: thesis: ex k being Element of NAT st x in A . (m + k)
take 0 ; :: thesis: x in A . (m + 0 )
thus x in A . (m + 0 ) by A1, A3; :: thesis: verum

end;

hence x in lim_sup A by Th8; :: thesis: verum

end;