let H be Element of QC-WFF ; :: thesis: for k being Element of NAT
for P being QC-pred_symbol of k
for V being QC-variable_list of holds
( H is_subformula_of P ! V iff H = P ! V )
let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for V being QC-variable_list of holds
( H is_subformula_of P ! V iff H = P ! V )
let P be QC-pred_symbol of k; :: thesis: for V being QC-variable_list of holds
( H is_subformula_of P ! V iff H = P ! V )
let V be QC-variable_list of ; :: thesis: ( H is_subformula_of P ! V iff H = P ! V )
thus ( H is_subformula_of P ! V implies H = P ! V ) :: thesis: ( H = P ! V implies H is_subformula_of P ! V )

proof

assume A1: H is_subformula_of P ! V ; :: thesis: H = P ! V
assume H <> P ! V ; :: thesis: contradiction
then H is_proper_subformula_of P ! V by A1, Def22;
then ex F being Element of QC-WFF st F is_immediate_constituent_of P ! V by Th75;
hence contradiction by Th59; :: thesis: verum

end;

thus ( H = P ! V implies H is_subformula_of P ! V ) ; :: thesis: verum