let F be Element of QC-WFF ; :: 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 Element of NAT st (@ F) . 1 is QC-pred_symbol of k by Th49;
hence ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 ) by Th48; :: thesis: verum