let s be Element of S; :: thesis: ( s is relational implies s is low-compounding )
assume s is relational ; :: thesis: s is low-compounding
then ( s in RelSymbolsOf S & RelSymbolsOf S c= LowerCompoundersOf S ) by Def17, Th1;
hence s is low-compounding by Def15; :: thesis: verum