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:10;

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:79;
hence contradiction by QC_LANG1:18, QC_LANG1:def 19; :: 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:79;
hence contradiction by QC_LANG1:18, QC_LANG1:def 18; :: 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:79;
hence contradiction by QC_LANG1:18, QC_LANG1:def 18; :: 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:79;
hence contradiction by QC_LANG1:18, QC_LANG1:def 17; :: 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