:: deftheorem Def21 defines Sub_& SUBSTUT1:def 21 :
for A being QC-alphabet
for S, S9 being Element of QC-Sub-WFF A st S `2 = S9 `2 holds
Sub_& (S,S9) = [((S `1) '&' (S9 `1)),(S `2)];