let f, g, h be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Omega g & g in Big_Omega h implies f in Big_Omega h )
assume ( f in Big_Omega g & g in Big_Omega h ) ; :: thesis: f in Big_Omega h
then ( h in Big_Oh g & g in Big_Oh f ) by Th19;
then h in Big_Oh f by Th12;
hence f in Big_Omega h by Th19; :: thesis: verum