theorem Th26: :: SUBSTUT1:26

for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 )