:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
for b₃ being Element of QC-Sub-WFF A holds
( b₃ = Sub_the_right_argument_of S iff ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b₃) & S9 `2 = b<sub>3</sub> `2 ) );