let k be Element of NAT ; :: thesis: for l being CQC-variable_list of
for P being QC-pred_symbol of k holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )]}
let l be CQC-variable_list of ; :: thesis: for P being QC-pred_symbol of k holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )]}
let P be QC-pred_symbol of k; :: thesis: SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )]}
A1: P ! l is atomic by QC_LANG1:def 17;

now

let x be set ; :: thesis: ( ( x in SepQuadruples (P ! l) implies x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )] ) & ( x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )] implies x in SepQuadruples (P ! l) ) )
thus ( x in SepQuadruples (P ! l) implies x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )] ) :: thesis: ( x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )] implies x in SepQuadruples (P ! l) )

proof

assume A2: x in SepQuadruples (P ! l) ; :: thesis: x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )]
then consider q being Element of CQC-WFF , k being Element of NAT , K being Finite_Subset of bound_QC-variables , f being Element of Funcs bound_QC-variables ,bound_QC-variables such that
A3: x = [q,k,K,f] by DOMAIN_1:31;

A4: now

assume [('not' q),k,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
then 'not' q is_subformula_of P ! l by Th36;
then 'not' q = P ! l by QC_LANG2:100;
then P ! l is negative by QC_LANG1:def 18;
hence contradiction by A1, QC_LANG1:51; :: thesis: verum

end;

A5: now

given r being Element of CQC-WFF such that A6: [(q '&' r),k,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
q '&' r is_subformula_of P ! l by A6, Th36;
then q '&' r = P ! l by QC_LANG2:100;
then P ! l is conjunctive by QC_LANG1:def 19;
hence contradiction by A1, QC_LANG1:51; :: thesis: verum

end;

A7: now

given r being Element of CQC-WFF , i being Element of NAT such that k = i + (QuantNbr r) and
A8: [(r '&' q),i,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
r '&' q is_subformula_of P ! l by A8, Th36;
then r '&' q = P ! l by QC_LANG2:100;
then P ! l is conjunctive by QC_LANG1:def 19;
hence contradiction by A1, QC_LANG1:51; :: thesis: verum

end;

now

given x being Element of bound_QC-variables , i being Element of NAT , h being Element of Funcs bound_QC-variables ,bound_QC-variables such that ( i + 1 = k & h +* ({x} --> (x. i)) = f ) and
A9: ( [(All x,q),i,K,h] in SepQuadruples (P ! l) or [(All x,q),i,(K \ {.x.}),h] in SepQuadruples (P ! l) ) ; :: thesis: contradiction
All x,q is_subformula_of P ! l by A9, Th36;
then All x,q = P ! l by QC_LANG2:100;
then P ! l is universal by QC_LANG1:def 20;
hence contradiction by A1, QC_LANG1:51; :: thesis: verum

end;

hence x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )] by A2, A3, A4, A5, A7, Th35; :: thesis: verum

end;

thus ( x = [(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )] implies x in SepQuadruples (P ! l) ) by Th31; :: thesis: verum

end;

hence SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )]} by TARSKI:def 1; :: thesis: verum