theorem Th18: :: SUBSTUT1:18

for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_left_argument_of (Sub_& (S1,S2)) = S1