let seq be ExtREAL_sequence; :: thesis: lim_inf seq <= lim_sup seq
A1: lim (superior_realsequence seq) = lim_sup seq by Th36;
A2: inferior_realsequence seq is convergent by Th37;
A3: now :: thesis: for n being Nat holds (inferior_realsequence seq) . n <= (superior_realsequence seq) . n
let n be Nat; :: thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n
A4: seq . n <= (superior_realsequence seq) . n by Th8;
(inferior_realsequence seq) . n <= seq . n by Th8;
hence (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A4, XXREAL_0:2; :: thesis: verum
end;
A5: lim (inferior_realsequence seq) = lim_inf seq by Th37;
superior_realsequence seq is convergent by Th36;
hence lim_inf seq <= lim_sup seq by A1, A2, A5, A3, Th38; :: thesis: verum