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

for x being object holds

( x in F iff x in lim_sup B )

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

assume A4:
F = Intersection (superior_setsequence B)
; :: thesis: F = lim_sup Bassume 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) )

end;for x being object holds

( x in F iff x in Intersection (superior_setsequence B) )

proof

hence
F = Intersection (superior_setsequence B)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in F iff x in Intersection (superior_setsequence B) )

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

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

for m being Nat holds x in (superior_setsequence B) . m

end;for m being Nat holds x in (superior_setsequence B) . m

proof

hence
x in Intersection (superior_setsequence B)
by PROB_1:13; :: thesis: verum
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;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

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

hence
x in F
by A1, KURATO_0:5; :: thesis: verumlet 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;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

for x being object holds

( x in F iff x in lim_sup B )

proof

hence
F = lim_sup B
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in F iff x in lim_sup B )

for m being Nat holds x in (superior_setsequence B) . m

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

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

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

hence
x in lim_sup B
by KURATO_0:5; :: thesis: verumlet 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;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

for m being Nat holds x in (superior_setsequence B) . m

proof

hence
x in F
by A4, PROB_1:13; :: thesis: verum
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;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