let S be Element of QC-Sub-WFF ; :: thesis: ( S is Sub_atomic implies ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) )
assume S is Sub_atomic ; :: thesis: ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 )
then ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k by Th25;
hence ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) by QC_LANG1:48; :: thesis: verum