let F be Subset of X; :: thesis: ( F = lim_sup B iff F = Intersection (superior_setsequence B) )

hereby :: thesis: ( F = Intersection (superior_setsequence B) implies F = lim_sup B )

assume B: F = lim_sup B ; :: thesis: F = Intersection (superior_setsequence B)
for x being set holds
( x in F iff x in Intersection (superior_setsequence B) )

proof

let x be set ; :: thesis: ( x in F iff x in Intersection (superior_setsequence B) )

hereby :: thesis: ( x in Intersection (superior_setsequence B) implies x in F )

assume x in F ; :: thesis: x in Intersection (superior_setsequence B)
then C00: for n being Element of NAT ex k being Element of NAT st x in B . (n + k) by B, KURATO_2:8;
for m being Element of NAT holds x in (superior_setsequence B) . m

proof

let m be Element of NAT ; :: thesis: x in (superior_setsequence B) . m
ex k being Element of NAT st x in B . (m + k) by C00;
hence x in (superior_setsequence B) . m by Th22; :: thesis: verum

end;

hence x in Intersection (superior_setsequence B) by PROB_1:29; :: thesis: verum

end;

assume B01: x in Intersection (superior_setsequence B) ; :: thesis: x in F

now

let m be Element of NAT ; :: thesis: ex k being Element of NAT st x in B . (m + k)
x in (superior_setsequence B) . m by B01, PROB_1:29;
hence ex k being Element of NAT st x in B . (m + k) by Th22; :: thesis: verum

end;

hence x in F by B, KURATO_2:8; :: thesis: verum

end;

hence F = Intersection (superior_setsequence B) by TARSKI:2; :: thesis: verum

end;

assume B: F = Intersection (superior_setsequence B) ; :: thesis: F = lim_sup B
for x being set holds
( x in F iff x in lim_sup B )

proof

let x be set ; :: thesis: ( x in F iff x in lim_sup B )

hereby :: thesis: ( x in lim_sup B implies x in F )

assume A0: x in F ; :: thesis: x in lim_sup B

now

let m be Element of NAT ; :: thesis: ex k being Element of NAT st x in B . (m + k)
x in (superior_setsequence B) . m by A0, B, PROB_1:29;
hence ex k being Element of NAT st x in B . (m + k) by Th22; :: thesis: verum

end;

hence x in lim_sup B by KURATO_2:8; :: thesis: verum

end;

assume x in lim_sup B ; :: thesis: x in F
then C00: for n being Element of NAT ex k being Element of NAT st x in B . (n + k) by KURATO_2:8;
for m being Element of NAT holds x in (superior_setsequence B) . m

proof

let m be Element of NAT ; :: thesis: x in (superior_setsequence B) . m
ex k being Element of NAT st x in B . (m + k) by C00;
hence x in (superior_setsequence B) . m by Th22; :: thesis: verum

end;

hence x in F by B, PROB_1:29; :: thesis: verum

end;

hence F = lim_sup B by TARSKI:2; :: thesis: verum