let A be QC-alphabet ; :: thesis: for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(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 Subformulae (P ! V) = {(P ! V)}
let P be QC-pred_symbol of k,A; :: thesis: for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}
let V be QC-variable_list of k,A; :: thesis: Subformulae (P ! V) = {(P ! V)}
thus Subformulae (P ! V) c= {(P ! V)} :: according to XBOOLE_0:def 10 :: thesis: {(P ! V)} c= Subformulae (P ! V)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae (P ! V) or a in {(P ! V)} )
assume a in Subformulae (P ! V) ; :: thesis: a in {(P ! V)}
then consider F being Element of QC-WFF A such that
A1: F = a and
A2: F is_subformula_of P ! V by Def22;
F = P ! V by A2, Th80;
hence a in {(P ! V)} by A1, TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(P ! V)} or a in Subformulae (P ! V) )
assume a in {(P ! V)} ; :: thesis: a in Subformulae (P ! V)
then a = P ! V by TARSKI:def 1;
hence a in Subformulae (P ! V) by Def22; :: thesis: verum