let A be QC-alphabet ; :: thesis: SepQuadruples (VERUM A) = {[(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}

now :: thesis: for x being object holds
( ( x in SepQuadruples (VERUM A) implies x = [(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] ) & ( x = [(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] implies x in SepQuadruples (VERUM A) ) )

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

proof

assume A1: x in SepQuadruples (VERUM A) ; :: thesis: x = [(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]
then consider q being Element of CQC-WFF A, t being QC-symbol of A, K being Element of Fin (bound_QC-variables A), f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) such that
A2: x = [q,t,K,f] by DOMAIN_1:10;

A3: now :: thesis: for x being Element of bound_QC-variables A
for v being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds
( not v ++ = t or not h +* ({x} --> (x. v)) = f or ( not [(All (x,q)),v,K,h] in SepQuadruples (VERUM A) & not [(All (x,q)),v,(K \ {.x.}),h] in SepQuadruples (VERUM A) ) )

given x being Element of bound_QC-variables A, v being QC-symbol of A, h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) such that v ++ = t and
h +* ({x} --> (x. v)) = f and
A4: ( [(All (x,q)),v,K,h] in SepQuadruples (VERUM A) or [(All (x,q)),v,(K \ {.x.}),h] in SepQuadruples (VERUM A) ) ; :: thesis: contradiction
All (x,q) is_subformula_of VERUM A by A4, Th35;
then All (x,q) = VERUM A by QC_LANG2:79;
then VERUM A is universal by QC_LANG1:def 21;
hence contradiction by QC_LANG1:20; :: thesis: verum

end;

A5: now :: thesis: for r being Element of CQC-WFF A
for v being QC-symbol of A holds
( not t = v + (QuantNbr r) or not [(r '&' q),v,K,f] in SepQuadruples (VERUM A) )

given r being Element of CQC-WFF A, v being QC-symbol of A such that t = v + (QuantNbr r) and
A6: [(r '&' q),v,K,f] in SepQuadruples (VERUM A) ; :: thesis: contradiction
r '&' q is_subformula_of VERUM A by A6, Th35;
then r '&' q = VERUM A by QC_LANG2:79;
then VERUM A is conjunctive by QC_LANG1:def 20;
hence contradiction by QC_LANG1:20; :: thesis: verum

end;

A7: now :: thesis: for r being Element of CQC-WFF A holds not [(q '&' r),t,K,f] in SepQuadruples (VERUM A)

given r being Element of CQC-WFF A such that A8: [(q '&' r),t,K,f] in SepQuadruples (VERUM A) ; :: thesis: contradiction
q '&' r is_subformula_of VERUM A by A8, Th35;
then q '&' r = VERUM A by QC_LANG2:79;
then VERUM A is conjunctive by QC_LANG1:def 20;
hence contradiction by QC_LANG1:20; :: thesis: verum

end;

A9: now :: thesis: not [('not' q),t,K,f] in SepQuadruples (VERUM A)

assume [('not' q),t,K,f] in SepQuadruples (VERUM A) ; :: thesis: contradiction
then 'not' q is_subformula_of VERUM A by Th35;
then 'not' q = VERUM A by QC_LANG2:79;
then VERUM A is negative by QC_LANG1:def 19;
hence contradiction by QC_LANG1:20; :: thesis: verum

end;

A10: index (VERUM A) = 0 A by Th22;
set p = VERUM A;
( [q,t,K,f] = [(VERUM A),(index (VERUM A)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples (VERUM A) or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples (VERUM A) or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples (VERUM A) ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples (VERUM A) or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples (VERUM A) ) ) ) by A1, A2, Th34;
hence x = [(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] by A2, A7, A5, A3, A9, A10; :: thesis: verum

end;

index (VERUM A) = 0 A by Th22;
hence ( x = [(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] implies x in SepQuadruples (VERUM A) ) by Th30; :: thesis: verum

end;

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