To use the extracted term E from a (complete) theorem T in another theorem, make E a DEF:

E==term_of(T).