let f, g, h be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Theta g & g in Big_Theta h implies f in Big_Theta h )
assume A1: ( f in Big_Theta g & g in Big_Theta h ) ; :: thesis: f in Big_Theta h
then ( f in Big_Omega g & g in Big_Omega h ) by XBOOLE_0:def 4;
then A2: f in Big_Omega h by Th21;
( f in Big_Oh g & g in Big_Oh h ) by A1, XBOOLE_0:def 4;
then f in Big_Oh h by Th12;
hence f in Big_Theta h by A2, XBOOLE_0:def 4; :: thesis: verum