for f, g being eventually-nonnegative Real_Sequence holds
( f in Big_Omega g iff g in Big_Oh f )