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 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 A2: x in F ; :: thesis: x in Intersection (superior_setsequence B)
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 A1, A2, KURATO_2:8;
hence x in (superior_setsequence B) . m by Th20; :: thesis: verum

end;

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

end;

assume A3: 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 A3, PROB_1:29;
hence ex k being Element of NAT st x in B . (m + k) by Th20; :: thesis: verum

end;

hence x in F by A1, KURATO_2:8; :: 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 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 A5: 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 A4, A5, PROB_1:29;
hence ex k being Element of NAT st x in B . (m + k) by Th20; :: thesis: verum

end;

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

end;

assume A6: x in lim_sup B ; :: thesis: x in F
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 A6, KURATO_2:8;
hence x in (superior_setsequence B) . m by Th20; :: thesis: verum

end;

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

end;

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