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) ) )

hence
SepQuadruples (VERUM A) = {[(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}
by TARSKI:def 1; :: thesis: verum( ( 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) )

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

index (VERUM A) = 0 A
by Th22;
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;

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;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) ) )

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

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) )

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

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

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

A10:
index (VERUM A) = 0 A
by Th22;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;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

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

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