let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for V being QC-variable_list of holds Subformulae (P ! V) = {(P ! V)}
let P be QC-pred_symbol of k; :: thesis: for V being QC-variable_list of holds Subformulae (P ! V) = {(P ! V)}
let V be QC-variable_list of ; :: 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 set ; :: 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 such that
A1: ( F = a & F is_subformula_of P ! V ) by Def23;
F = P ! V by A1, Th100;
hence a in {(P ! V)} by A1, TARSKI:def 1; :: thesis: verum

end;

let a be set ; :: 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 & P ! V is_subformula_of P ! V ) by TARSKI:def 1;
hence a in Subformulae (P ! V) by Def23; :: thesis: verum