let f be eventually-nonnegative Real_Sequence; :: thesis: f in Big_Omega f
f in Big_Oh f by Th10;
hence f in Big_Omega f by Th19; :: thesis: verum