let A be QC-alphabet ; :: thesis: SepQuadruples () = {[(),(0 A),(),()]}
now :: thesis: for x being object holds
( ( x in SepQuadruples () implies x = [(),(0 A),(),()] ) & ( x = [(),(0 A),(),()] implies x in SepQuadruples () ) )
let x be object ; :: thesis: ( ( x in SepQuadruples () implies x = [(),(0 A),(),()] ) & ( x = [(),(0 A),(),()] implies x in SepQuadruples () ) )
thus ( x in SepQuadruples () implies x = [(),(0 A),(),()] ) :: thesis: ( x = [(),(0 A),(),()] implies x in SepQuadruples () )
proof
assume A1: x in SepQuadruples () ; :: thesis: x = [(),(0 A),(),()]
then consider q being Element of CQC-WFF A, t being QC-symbol of A, K being Element of Fin , f being Element of Funcs (,) 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 (,) holds
( not v ++ = t or not h +* ({x} --> (x. v)) = f or ( not [(All (x,q)),v,K,h] in SepQuadruples () & not [(All (x,q)),v,(K \ {.x.}),h] in SepQuadruples () ) )
given x being Element of bound_QC-variables A, v being QC-symbol of A, h being Element of Funcs (,) such that v ++ = t and
h +* ({x} --> (x. v)) = f and
A4: ( [(All (x,q)),v,K,h] in SepQuadruples () or [(All (x,q)),v,(K \ {.x.}),h] in SepQuadruples () ) ; :: thesis: contradiction
All (x,q) is_subformula_of VERUM A by ;
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 + () or not [(r '&' q),v,K,f] in SepQuadruples () )
given r being Element of CQC-WFF A, v being QC-symbol of A such that t = v + () and
r '&' q is_subformula_of VERUM A by ;
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 ()end;
A10: index () = 0 A by Th22;
set p = VERUM A;
( [q,t,K,f] = [(),(index ()),(),()] or [(),t,K,f] in SepQuadruples () or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples () or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + () & [(r '&' q),u,K,f] in SepQuadruples () ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs (,) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples () or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples () ) ) ) by A1, A2, Th34;
hence x = [(),(0 A),(),()] by A2, A7, A5, A3, A9, A10; :: thesis: verum
end;
index () = 0 A by Th22;
hence ( x = [(),(0 A),(),()] implies x in SepQuadruples () ) by Th30; :: thesis: verum
end;
hence SepQuadruples () = {[(),(0 A),(),()]} by TARSKI:def 1; :: thesis: verum