let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al holds
( X |- p iff X \/ {('not' p)} is Inconsistent )
let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al holds
( X |- p iff X \/ {('not' p)} is Inconsistent )
let p be Element of CQC-WFF Al; :: thesis: ( X |- p iff X \/ {('not' p)} is Inconsistent )
thus ( X |- p implies X \/ {('not' p)} is Inconsistent ) :: thesis: ( X \/ {('not' p)} is Inconsistent implies X |- p )

proof

assume X |- p ; :: thesis: X \/ {('not' p)} is Inconsistent
then consider f being FinSequence of CQC-WFF Al such that
A1: rng f c= X and
A2: |- f ^ <*p*> ;
set f2 = f ^ <*('not' p)*>;
set f1 = (f ^ <*('not' p)*>) ^ <*('not' p)*>;
A3: Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' p)*> by CALCUL_1:5;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom <*('not' p)*> by FINSEQ_1:38;
then A4: (len f) + 1 in dom (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) by A3, FINSEQ_1:28;
Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p by CALCUL_1:5;
then (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 1) = Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A3, FINSEQ_1:42;
then Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) is_tail_of Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A4, CALCUL_1:def 16;
then A5: |- (f ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_1:33;
A6: 0 + 1 <= len (f ^ <*('not' p)*>) by CALCUL_1:10;
( Ant (f ^ <*('not' p)*>) = f & Suc (f ^ <*('not' p)*>) = 'not' p ) by CALCUL_1:5;
then A7: rng (f ^ <*('not' p)*>) = (rng f) \/ {('not' p)} by A6, CALCUL_1:3;
|- (f ^ <*('not' p)*>) ^ <*p*> by A2, Th5;
then not f ^ <*('not' p)*> is Consistent by A5;
hence X \/ {('not' p)} is Inconsistent by A1, A7, Th4, XBOOLE_1:9; :: thesis: verum

end;

thus ( X \/ {('not' p)} is Inconsistent implies X |- p ) :: thesis: verum

proof

assume X \/ {('not' p)} is Inconsistent ; :: thesis: X |- p
then X \/ {('not' p)} |- p by Th6;
then consider f being FinSequence of CQC-WFF Al such that
A8: rng f c= X \/ {('not' p)} and
A9: |- f ^ <*p*> ;

now :: thesis: ( not rng f c= X implies X |- p )

set g = f - {('not' p)};
reconsider A = f " {('not' p)} as finite set ;
reconsider B = dom f as finite set ;
set n = card A;
set h = (f - {('not' p)}) ^ (IdFinS (('not' p),(card A)));
A10: len (IdFinS (('not' p),(card A))) = card A by CARD_1:def 7;
A c= B by RELAT_1:132;
then A c= Seg (len f) by FINSEQ_1:def 3;
then a11: A is included_in_Seg by FINSEQ_1:def 13;

A12: now :: thesis: for i being Nat st i in seq ((len (f - {('not' p)})),(card A)) holds
i - (len (f - {('not' p)})) in dom (Sgm A)

let i be Nat; :: thesis: ( i in seq ((len (f - {('not' p)})),(card A)) implies i - (len (f - {('not' p)})) in dom (Sgm A) )
reconsider j = i - (len (f - {('not' p)})) as Integer ;
assume A13: i in seq ((len (f - {('not' p)})),(card A)) ; :: thesis: i - (len (f - {('not' p)})) in dom (Sgm A)
then A14: 1 + (len (f - {('not' p)})) <= i by CALCUL_2:1;
then A15: 1 <= j by XREAL_1:19;
i <= (card A) + (len (f - {('not' p)})) by A13, CALCUL_2:1;
then A16: j <= card A by XREAL_1:20;
0 <= j by A14, XREAL_1:19;
then reconsider j = j as Element of NAT by INT_1:3;
j in Seg (card A) by A15, A16, FINSEQ_1:1;
hence i - (len (f - {('not' p)})) in dom (Sgm A) by a11, FINSEQ_3:40; :: thesis: verum

end;

assume not rng f c= X ; :: thesis: X |- p
then consider a being object such that
A17: a in rng f and
A18: not a in X ;
( a in X or a in {('not' p)} ) by A8, A17, XBOOLE_0:def 3;
then a = 'not' p by A18, TARSKI:def 1;
then consider i being Nat such that
A19: i in B and
A20: f . i = 'not' p by A17, FINSEQ_2:10;
reconsider C = B \ A as finite set ;
defpred S₁[ Nat, object ] means ( ( $1 in Seg (len (f - {('not' p)})) implies $2 = (Sgm (B \ A)) . $1 ) & ( $1 in seq ((len (f - {('not' p)})),(card A)) implies $2 = (Sgm A) . ($1 - (len (f - {('not' p)}))) ) );
A21: card C = (card B) - (card A) by CARD_2:44, RELAT_1:132
.= (card (Seg (len f))) - (card A) by FINSEQ_1:def 3
.= (len f) - (card A) by FINSEQ_1:57
.= len (f - {('not' p)}) by FINSEQ_3:59 ;
A22: for k being Nat st k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) holds
ex a being object st S₁[k,a]

proof

let k be Nat; :: thesis: ( k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) implies ex a being object st S₁[k,a] )
assume k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) ; :: thesis: ex a being object st S₁[k,a]

now :: thesis: ( k in Seg (len (f - {('not' p)})) implies ex a being set st S₁[k,a] )

assume A23: k in Seg (len (f - {('not' p)})) ; :: thesis: ex a being set st S₁[k,a]
take a = (Sgm (B \ A)) . k; :: thesis: S₁[k,a]
Seg (len (f - {('not' p)})) misses seq ((len (f - {('not' p)})),(card A)) by CALCUL_2:8;
hence S₁[k,a] by A23, XBOOLE_0:3; :: thesis: verum

end;

hence ex a being object st S₁[k,a] ; :: thesis: verum

end;

consider F being FinSequence such that
A24: ( dom F = Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) & ( for k being Nat st k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) holds
S₁[k,F . k] ) ) from FINSEQ_1:sch 1(A22);
A26: dom (Sgm C) = Seg (card C) by FINSEQ_3:40;
A27: rng F = B

proof

now :: thesis: for a being object st a in rng F holds
a in B

let a be object ; :: thesis: ( a in rng F implies a in B )
assume a in rng F ; :: thesis: a in B
then consider i being Nat such that
A28: i in dom F and
A29: F . i = a by FINSEQ_2:10;

A30: now :: thesis: ( i in Seg (len (f - {('not' p)})) implies a in B )

assume i in Seg (len (f - {('not' p)})) ; :: thesis: a in B
then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A24, A21, A28, A29, FINSEQ_3:40;
then a in rng (Sgm C) by FUNCT_1:3;
then a in C by FINSEQ_1:def 14;
hence a in B ; :: thesis: verum

end;

A31: now :: thesis: ( i in seq ((len (f - {('not' p)})),(card A)) implies a in B )

A32: rng (Sgm A) = A by a11, FINSEQ_1:def 14;
A33: A c= B by RELAT_1:132;
assume A34: i in seq ((len (f - {('not' p)})),(card A)) ; :: thesis: a in B
then a = (Sgm A) . (i - (len (f - {('not' p)}))) by A24, A28, A29;
then a in A by A12, A34, A32, FUNCT_1:3;
hence a in B by A33; :: thesis: verum

end;

i in (Seg (len (f - {('not' p)}))) \/ (seq ((len (f - {('not' p)})),(card A))) by A10, A24, A28, Lm1;
hence a in B by A30, A31, XBOOLE_0:def 3; :: thesis: verum

end;

hence rng F c= B ; :: according to XBOOLE_0:def 10 :: thesis: B c= rng F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in rng F )
assume A35: a in B ; :: thesis: a in rng F

A36: now :: thesis: ( not a in A implies a in rng F )

assume not a in A ; :: thesis: a in rng F
then a in C by A35, XBOOLE_0:def 5;
then a in rng (Sgm C) by FINSEQ_1:def 14;
then consider i being Nat such that
A38: i in dom (Sgm C) and
A39: (Sgm C) . i = a by FINSEQ_2:10;
A40: 1 <= i by A38, FINSEQ_3:25;
len (Sgm C) = len (f - {('not' p)}) by A26, A21, FINSEQ_1:def 3;
then A41: i <= len (f - {('not' p)}) by A38, FINSEQ_3:25;
len (f - {('not' p)}) <= len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by CALCUL_1:6;
then i <= len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by A41, XXREAL_0:2;
then A42: i in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) by A40, FINSEQ_1:1;
i in Seg (len (f - {('not' p)})) by A40, A41, FINSEQ_1:1;
then a = F . i by A24, A39, A42;
hence a in rng F by A24, A42, FUNCT_1:3; :: thesis: verum

end;

now :: thesis: ( a in A implies a in rng F )

assume A43: a in A ; :: thesis: a in rng F
rng (Sgm A) = A by a11, FINSEQ_1:def 14;
then consider i being Nat such that
A44: i in dom (Sgm A) and
A45: (Sgm A) . i = a by A43, FINSEQ_2:10;
reconsider i = i as Nat ;
set m = i + (len (f - {('not' p)}));
len (Sgm A) = card A by a11, FINSEQ_3:39;
then i <= card A by A44, FINSEQ_3:25;
then A46: i + (len (f - {('not' p)})) <= (card A) + (len (f - {('not' p)})) by XREAL_1:6;
then i + (len (f - {('not' p)})) <= (len (f - {('not' p)})) + (len (IdFinS (('not' p),(card A)))) by CARD_1:def 7;
then A47: i + (len (f - {('not' p)})) <= len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by FINSEQ_1:22;
A48: 1 <= i by A44, FINSEQ_3:25;
then 1 + (len (f - {('not' p)})) <= i + (len (f - {('not' p)})) by XREAL_1:6;
then A49: i + (len (f - {('not' p)})) in seq ((len (f - {('not' p)})),(card A)) by A46, CALCUL_2:1;
i <= i + (len (f - {('not' p)})) by NAT_1:11;
then 1 <= i + (len (f - {('not' p)})) by A48, XXREAL_0:2;
then i + (len (f - {('not' p)})) in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by A47, FINSEQ_3:25;
then A50: i + (len (f - {('not' p)})) in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) by FINSEQ_1:def 3;
a = (Sgm A) . ((i + (len (f - {('not' p)}))) - (len (f - {('not' p)}))) by A45;
then a = F . (i + (len (f - {('not' p)}))) by A24, A49, A50;
hence a in rng F by A24, A50, FUNCT_1:3; :: thesis: verum

end;

hence a in rng F by A36; :: thesis: verum

end;

A51: len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) = (len (f - {('not' p)})) + (len (IdFinS (('not' p),(card A)))) by FINSEQ_1:22
.= ((len f) - (card A)) + (len (IdFinS (('not' p),(card A)))) by FINSEQ_3:59
.= ((len f) - (card A)) + (card A) by CARD_1:def 7
.= len f ;
then A52: dom F = B by A24, FINSEQ_1:def 3;
then reconsider F = F as Relation of B,B by A27, RELSET_1:4;
rng F c= B ;
then reconsider F = F as Function of B,B by A52, FUNCT_2:2;
F is one-to-one

proof

let a1, a2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a1 in dom F or not a2 in dom F or not F . a1 = F . a2 or a1 = a2 )
assume that
A53: a1 in dom F and
A54: a2 in dom F and
A55: F . a1 = F . a2 ; :: thesis: a1 = a2
A56: a2 in (Seg (len (f - {('not' p)}))) \/ (seq ((len (f - {('not' p)})),(card A))) by A10, A24, A54, Lm1;

A57: now :: thesis: ( a1 in Seg (len (f - {('not' p)})) implies a1 = a2 )

assume A58: a1 in Seg (len (f - {('not' p)})) ; :: thesis: a1 = a2
then A59: a1 in dom (Sgm C) by A21, FINSEQ_3:40;
F . a1 = (Sgm C) . a1 by A24, A53, A58;
then F . a1 in rng (Sgm C) by A59, FUNCT_1:3;
then A60: F . a1 in C by FINSEQ_1:def 14;

A61: now :: thesis: not a2 in seq ((len (f - {('not' p)})),(card A))

assume A62: a2 in seq ((len (f - {('not' p)})),(card A)) ; :: thesis: contradiction
then reconsider i = a2 as Nat ;
(Sgm A) . (i - (len (f - {('not' p)}))) in rng (Sgm A) by A12, A62, FUNCT_1:3;
then F . a2 in rng (Sgm A) by A24, A54, A62;
then F . a2 in A by a11, FINSEQ_1:def 14;
hence contradiction by A55, A60, XBOOLE_0:def 5; :: thesis: verum

end;

now :: thesis: ( a2 in Seg (len (f - {('not' p)})) implies a1 = a2 )

assume A63: a2 in Seg (len (f - {('not' p)})) ; :: thesis: a1 = a2
then F . a2 = (Sgm C) . a2 by A24, A54;
then A64: (Sgm C) . a1 = (Sgm C) . a2 by A24, A53, A55, A58;
A65: Sgm C is one-to-one by FINSEQ_3:92;
a2 in dom (Sgm C) by A21, A63, FINSEQ_3:40;
hence a1 = a2 by A59, A64, A65; :: thesis: verum

end;

hence a1 = a2 by A56, A61, XBOOLE_0:def 3; :: thesis: verum

end;

A66: now :: thesis: ( a1 in seq ((len (f - {('not' p)})),(card A)) implies a1 = a2 )

assume A67: a1 in seq ((len (f - {('not' p)})),(card A)) ; :: thesis: a1 = a2
then reconsider i = a1 as Nat ;
A68: i - (len (f - {('not' p)})) in dom (Sgm A) by A12, A67;

A69: now :: thesis: ( a2 in seq ((len (f - {('not' p)})),(card A)) implies a1 = a2 )

assume A70: a2 in seq ((len (f - {('not' p)})),(card A)) ; :: thesis: a1 = a2
then reconsider i1 = a2 as Nat ;
F . a2 = (Sgm A) . (i1 - (len (f - {('not' p)}))) by A24, A54, A70;
then A71: (Sgm A) . (i1 - (len (f - {('not' p)}))) = (Sgm A) . (i - (len (f - {('not' p)}))) by A24, A53, A55, A67;
A72: Sgm A is one-to-one by a11, FINSEQ_3:92;
i1 - (len (f - {('not' p)})) in dom (Sgm A) by A12, A70;
then i1 - (len (f - {('not' p)})) = i - (len (f - {('not' p)})) by A68, A71, A72;
hence a1 = a2 ; :: thesis: verum

end;

(Sgm A) . (i - (len (f - {('not' p)}))) in rng (Sgm A) by A12, A67, FUNCT_1:3;
then F . a1 in rng (Sgm A) by A24, A53, A67;
then A73: F . a1 in A by a11, FINSEQ_1:def 14;

now :: thesis: not a2 in Seg (len (f - {('not' p)}))

assume a2 in Seg (len (f - {('not' p)})) ; :: thesis: contradiction
then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A24, A21, A54, FINSEQ_3:40;
then F . a2 in rng (Sgm C) by FUNCT_1:3;
then F . a2 in C by FINSEQ_1:def 14;
hence contradiction by A55, A73, XBOOLE_0:def 5; :: thesis: verum

end;

hence a1 = a2 by A56, A69, XBOOLE_0:def 3; :: thesis: verum

end;

a1 in (Seg (len (f - {('not' p)}))) \/ (seq ((len (f - {('not' p)})),(card A))) by A10, A24, A53, Lm1;
hence a1 = a2 by A57, A66, XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider F = F as Permutation of (dom f) by A27, FUNCT_2:57;
consider j being Nat such that
A74: j in dom F and
A75: F . j = i by A27, A19, FINSEQ_2:10;
A76: dom (Per (f,F)) = B by CALCUL_2:19
.= dom F by A24, A51, FINSEQ_1:def 3
.= dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by A24, FINSEQ_1:def 3 ;

A77: now :: thesis: for k being Nat st k in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) holds
(Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k

let k be Nat; :: thesis: ( k in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) implies (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k )
assume A78: k in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) ; :: thesis: (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k
A79: k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) by A78, FINSEQ_1:def 3;

A80: now :: thesis: ( ex i being Nat st
( i in dom (IdFinS (('not' p),(card A))) & k = (len (f - {('not' p)})) + i ) implies (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k )

A81: k in dom (F * f) by A76, A78, CALCUL_2:def 2;
given i being Nat such that A82: i in dom (IdFinS (('not' p),(card A))) and
A83: k = (len (f - {('not' p)})) + i ; :: thesis: (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k
len (IdFinS (('not' p),(card A))) = card A by CARD_1:def 7;
then A84: i <= card A by A82, FINSEQ_3:25;
then A85: k <= (card A) + (len (f - {('not' p)})) by A83, XREAL_1:6;
A86: 1 <= i by A82, FINSEQ_3:25;
then 1 + (len (f - {('not' p)})) <= k by A83, XREAL_1:6;
then A87: k in seq ((len (f - {('not' p)})),(card A)) by A85, CALCUL_2:1;
then F . k = (Sgm A) . (k - (len (f - {('not' p)}))) by A24, A79;
then F . k in rng (Sgm A) by A12, A87, FUNCT_1:3;
then F . k in A by a11, FINSEQ_1:def 14;
then f . (F . k) in {('not' p)} by FUNCT_1:def 7;
then f . (F . k) = 'not' p by TARSKI:def 1;
then (F * f) . k = 'not' p by A81, FUNCT_1:12;
then A88: (Per (f,F)) . k = 'not' p by CALCUL_2:def 2;
i in Seg (card A) by A86, A84, FINSEQ_1:1;
hence (Per (f,F)) . k = (IdFinS (('not' p),(card A))) . i by A88, FUNCOP_1:7
.= ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k by A82, A83, FINSEQ_1:def 7 ;
:: thesis: verum

end;

now :: thesis: ( k in dom (f - {('not' p)}) implies (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k )

assume A89: k in dom (f - {('not' p)}) ; :: thesis: (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k
then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def 3;
k in Seg (len (f - {('not' p)})) by A89, FINSEQ_1:def 3;
then A91: F . k = (Sgm C) . k by A24, A79;
k in dom (F * f) by A76, A78, CALCUL_2:def 2;
then (F * f) . k = f . ((Sgm C) . k) by A91, FUNCT_1:12;
hence (Per (f,F)) . k = f . ((Sgm C) . k) by CALCUL_2:def 2
.= ((Sgm C) * f) . k by A90, FUNCT_1:13
.= (f - {('not' p)}) . k by FINSEQ_3:def 1
.= ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k by A89, FINSEQ_1:def 7 ;
:: thesis: verum

end;

hence (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k by A78, A80, FINSEQ_1:25; :: thesis: verum

end;

then A92: Per (f,F) = (f - {('not' p)}) ^ (IdFinS (('not' p),(card A))) by A76;
reconsider h = (f - {('not' p)}) ^ (IdFinS (('not' p),(card A))) as FinSequence of CQC-WFF Al by A76, A77, FINSEQ_1:13;
(F * f) . j = 'not' p by A20, A74, A75, FUNCT_1:13;
then A93: h . j = 'not' p by A92, CALCUL_2:def 2;

A94: now :: thesis: not j in dom (f - {('not' p)})

assume A95: j in dom (f - {('not' p)}) ; :: thesis: contradiction
then (f - {('not' p)}) . j = 'not' p by A93, FINSEQ_1:def 7;
then A96: (f - {('not' p)}) . j in {('not' p)} by TARSKI:def 1;
A97: rng (f - {('not' p)}) = (rng f) \ {('not' p)} by FINSEQ_3:65;
(f - {('not' p)}) . j in rng (f - {('not' p)}) by A95, FUNCT_1:3;
hence contradiction by A96, A97, XBOOLE_0:def 5; :: thesis: verum

end;

j in dom f by A74;
then j in dom h by A76, CALCUL_2:19;
then consider k being Nat such that
A98: k in dom (IdFinS (('not' p),(card A))) and
j = (len (f - {('not' p)})) + k by A94, FINSEQ_1:25;
reconsider g = f - {('not' p)} as FinSequence of CQC-WFF Al by FINSEQ_3:86;
( 1 <= k & k <= len (IdFinS (('not' p),(card A))) ) by A98, FINSEQ_3:25;
then 1 <= len (IdFinS (('not' p),(card A))) by XXREAL_0:2;
then A99: 1 <= card A by CARD_1:def 7;
|- h ^ <*p*> by A9, A92, CALCUL_2:30;
then A100: |- (g ^ <*('not' p)*>) ^ <*p*> by A99, CALCUL_2:32;
( rng g = (rng f) \ {('not' p)} & (rng f) \ {('not' p)} c= (X \/ {('not' p)}) \ {('not' p)} ) by A8, FINSEQ_3:65, XBOOLE_1:33;
then A101: rng g c= X \ {('not' p)} by XBOOLE_1:40;
X \ {('not' p)} c= X by XBOOLE_1:36;
then A102: rng g c= X by A101;
|- (g ^ <*p*>) ^ <*p*> by CALCUL_2:21;
then |- g ^ <*p*> by A100, CALCUL_2:26;
hence X |- p by A102; :: thesis: verum

end;

hence X |- p by A9; :: thesis: verum

end;