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

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

assume 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) )

proof

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

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

assume 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;

assume x in Union (inferior_setsequence B) ; :: thesis: x in F
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;

hence F = Union (inferior_setsequence B) by TARSKI:2; :: thesis: verum

end;

assume A4: F = Union (inferior_setsequence B) ; :: thesis: F = lim_inf B
for x being object holds
( x in F iff x in lim_inf B )

proof

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

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

assume 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;

assume x in lim_inf B ; :: thesis: x in F
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;

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