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;
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 &
h +* ({x} --> (x. l)) = f )
and A8:
(
[(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 A8, Th36;
then
All x,
q = VERUM
by QC_LANG2:99;
hence
contradiction
by QC_LANG1:51, QC_LANG1:def 20;
:: thesis: verum end;
hence
x = [VERUM ,0 ,({}. bound_QC-variables ),(id bound_QC-variables )]
by A1, A2, A3, A4, A6, 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