let F be Subset of X; :: thesis:

hereby :: thesis:

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

proof

let x be object ; :: thesis:

hereby :: thesis:

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

proof

let m be Nat; :: thesis:
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:

end;

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

end;

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

now :: thesis:

let m be Nat; :: thesis:
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:

end;

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

end;

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

end;

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

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A5: x in F ; :: thesis:

now :: thesis:

let m be Nat; :: thesis:
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:

end;

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

end;

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

proof

let m be Nat; :: thesis:
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:

end;

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

end;

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