now

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

proof

assume A1: x in SepQuadruples VERUM ; :: thesis: x = [VERUM ,0 ,({}. 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
A2: x = [q,k,K,f] by DOMAIN_1:31;

A3: now

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

end;

A5: now

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

end;

A7: now

given r being Element of CQC-WFF such that A8: [(q '&' r),k,K,f] in SepQuadruples VERUM ; :: thesis: contradiction
q '&' r is_subformula_of VERUM by A8, Th36;
then q '&' r = VERUM by QC_LANG2:99;
hence contradiction by QC_LANG1:51, QC_LANG1:def 19; :: thesis: verum

end;

now

assume [('not' q),k,K,f] in SepQuadruples VERUM ; :: thesis: contradiction
then 'not' q is_subformula_of VERUM by Th36;
then 'not' q = VERUM by QC_LANG2:99;
hence contradiction by QC_LANG1:51, QC_LANG1:def 18; :: thesis: verum

end;

hence x = [VERUM ,0 ,({}. bound_QC-variables ),(id bound_QC-variables )] by A1, A2, A7, A5, A3, Th23, Th35; :: thesis: verum

end;

thus ( x = [VERUM ,0 ,({}. bound_QC-variables ),(id bound_QC-variables )] implies x in SepQuadruples VERUM ) by Th23, Th31; :: thesis: verum

end;

hence SepQuadruples VERUM = {[VERUM ,0 ,({}. bound_QC-variables ),(id bound_QC-variables )]} by TARSKI:def 1; :: thesis: verum