let A be QC-alphabet ; :: thesis: for H, F being Element of QC-WFF A st H is atomic holds
not F is_proper_subformula_of H
let H, F be Element of QC-WFF A; :: thesis: ( H is atomic implies not F is_proper_subformula_of H )
assume ex k being Element of NAT ex P being QC-pred_symbol of k,A ex V being QC-variable_list of k,A st H = P ! V ; :: according to QC_LANG1:def 18 :: thesis: not F is_proper_subformula_of H
hence not F is_proper_subformula_of H by Th65; :: thesis: verum