let s be Element of S; :: thesis: ( s is operational implies s is low-compounding )
assume s is operational ; :: thesis: s is low-compounding
then ( s in OpSymbolsOf S & OpSymbolsOf S c= LowerCompoundersOf S ) by DefOperational, Lm8;
hence s is low-compounding by DefLowCompounding; :: thesis: verum