let F be Subset of X; :: thesis: ( F = lim_inf B iff F = Union (inferior_setsequence B) )

for x being object holds

( x in F iff x in lim_inf B )

hereby :: thesis: ( F = Union (inferior_setsequence B) implies F = lim_inf B )

assume A4:
F = Union (inferior_setsequence B)
; :: thesis: F = lim_inf Bassume A1:
F = lim_inf B
; :: thesis: F = Union (inferior_setsequence B)

for x being object holds

( x in F iff x in Union (inferior_setsequence B) )

end;for x being object holds

( x in F iff x in Union (inferior_setsequence B) )

proof

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

then consider n being Nat such that

A3: x in (inferior_setsequence B) . n by PROB_1:12;

for k being Nat holds x in B . (n + k) by A3, Th19;

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

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

assume
x in Union (inferior_setsequence B)
; :: thesis: x in Fassume
x in F
; :: thesis: x in Union (inferior_setsequence B)

then consider n being Nat such that

A2: for k being Nat holds x in B . (n + k) by A1, KURATO_0:4;

x in (inferior_setsequence B) . n by A2, Th19;

hence x in Union (inferior_setsequence B) by PROB_1:12; :: thesis: verum

end;then consider n being Nat such that

A2: for k being Nat holds x in B . (n + k) by A1, KURATO_0:4;

x in (inferior_setsequence B) . n by A2, Th19;

hence x in Union (inferior_setsequence B) by PROB_1:12; :: thesis: verum

then consider n being Nat such that

A3: x in (inferior_setsequence B) . n by PROB_1:12;

for k being Nat holds x in B . (n + k) by A3, Th19;

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

for x being object holds

( x in F iff x in lim_inf B )

proof

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

then consider n being Nat such that

A6: for k being Nat holds x in B . (n + k) by KURATO_0:4;

x in (inferior_setsequence B) . n by A6, Th19;

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

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

assume
x in lim_inf B
; :: thesis: x in Fassume
x in F
; :: thesis: x in lim_inf B

then consider n being Nat such that

A5: x in (inferior_setsequence B) . n by A4, PROB_1:12;

for k being Nat holds x in B . (n + k) by A5, Th19;

hence x in lim_inf B by KURATO_0:4; :: thesis: verum

end;then consider n being Nat such that

A5: x in (inferior_setsequence B) . n by A4, PROB_1:12;

for k being Nat holds x in B . (n + k) by A5, Th19;

hence x in lim_inf B by KURATO_0:4; :: thesis: verum

then consider n being Nat such that

A6: for k being Nat holds x in B . (n + k) by KURATO_0:4;

x in (inferior_setsequence B) . n by A6, Th19;

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