let H, F be Element of QC-WFF ; :: thesis: ( H is atomic implies not F is_immediate_constituent_of H )
assume ex k being Element of NAT ex P being QC-pred_symbol of k ex V being QC-variable_list of k st H = P ! V ; :: according to QC_LANG1:def 16 :: thesis: not F is_immediate_constituent_of H
hence not F is_immediate_constituent_of H by Th59; :: thesis: verum