:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :
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_left_argument_of S iff ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b₃,S9) & b₃ `2 = S9 `2 ) );