let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A
for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let H be Element of QC-WFF A; :: thesis: for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let P be QC-pred_symbol of k,A; :: thesis: for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let V be QC-variable_list of k,A; :: 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;
then ex F being Element of QC-WFF A st F is_immediate_constituent_of P ! V by Th55;
hence contradiction by Th42; :: thesis: verum
end;
thus ( H = P ! V implies H is_subformula_of P ! V ) ; :: thesis: verum