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