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 A1: F = lim_sup B ; :: thesis: F = Intersection (superior_setsequence B)
for x being object holds
( x in F iff x in Intersection (superior_setsequence B) )

proof

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

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

assume A2: x in F ; :: thesis: x in Intersection (superior_setsequence B)
for m being Nat holds x in (superior_setsequence B) . m

proof

let m be Nat; :: thesis: x in (superior_setsequence B) . m
ex k being Nat st x in B . (m + k) by A1, A2, KURATO_0:5;
hence x in (superior_setsequence B) . m by Th20; :: thesis: verum

end;

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

end;

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

now :: thesis: for m being Nat ex k being Nat st x in B . (m + k)

let m be Nat; :: thesis: ex k being Nat st x in B . (m + k)
x in (superior_setsequence B) . m by A3, PROB_1:13;
hence ex k being Nat st x in B . (m + k) by Th20; :: thesis: verum

end;

hence x in F by A1, KURATO_0:5; :: thesis: verum

end;

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

end;

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

proof

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

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

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

now :: thesis: for m being Nat ex k being Nat st x in B . (m + k)

let m be Nat; :: thesis: ex k being Nat st x in B . (m + k)
x in (superior_setsequence B) . m by A4, A5, PROB_1:13;
hence ex k being Nat st x in B . (m + k) by Th20; :: thesis: verum

end;

hence x in lim_sup B by KURATO_0:5; :: thesis: verum

end;

assume A6: x in lim_sup B ; :: thesis: x in F
for m being Nat holds x in (superior_setsequence B) . m

proof

let m be Nat; :: thesis: x in (superior_setsequence B) . m
ex k being Nat st x in B . (m + k) by A6, KURATO_0:5;
hence x in (superior_setsequence B) . m by Th20; :: thesis: verum

end;

hence x in F by A4, PROB_1:13; :: thesis: verum

end;

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