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