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