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