let A be QC-alphabet ; :: thesis: 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 )
let F be Element of QC-WFF A; :: thesis: ( F is atomic implies ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 ) )
assume F is atomic ; :: thesis: ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 )
then ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A by Th18;
hence ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 ) by Th17; :: thesis: verum