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