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

proof

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

end;

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

proof

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

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

set g = f - {p};
reconsider A = f " {p} as finite set ;
reconsider B = dom f as finite set ;
set n = card A;
set h = (f - {p}) ^ (IdFinS (p,(card A)));
A10: len (IdFinS (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 - {p})),(card A)) holds
i - (len (f - {p})) in dom (Sgm A)

let i be Nat; :: thesis: ( i in seq ((len (f - {p})),(card A)) implies i - (len (f - {p})) in dom (Sgm A) )
reconsider j = i - (len (f - {p})) as Integer ;
assume A13: i in seq ((len (f - {p})),(card A)) ; :: thesis: i - (len (f - {p})) in dom (Sgm A)
then A14: 1 + (len (f - {p})) <= i by CALCUL_2:1;
then A15: 1 <= j by XREAL_1:19;
i <= (card A) + (len (f - {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 - {p})) in dom (Sgm A) by a11, FINSEQ_3:40; :: thesis: verum

end;

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

proof

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

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

assume A23: k in Seg (len (f - {p})) ; :: thesis: ex a being set st S₁[k,a]
take a = (Sgm (B \ A)) . k; :: thesis: S₁[k,a]
Seg (len (f - {p})) misses seq ((len (f - {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 - {p}) ^ (IdFinS (p,(card A))))) & ( for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (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 - {p})) implies a in B )

assume i in Seg (len (f - {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 - {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 - {p})),(card A)) ; :: thesis: a in B
then a = (Sgm A) . (i - (len (f - {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 - {p}))) \/ (seq ((len (f - {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 - {p}) by A26, A21, FINSEQ_1:def 3;
then A41: i <= len (f - {p}) by A38, FINSEQ_3:25;
len (f - {p}) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by CALCUL_1:6;
then i <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by A41, XXREAL_0:2;
then A42: i in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A40, FINSEQ_1:1;
i in Seg (len (f - {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 - {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 - {p})) <= (card A) + (len (f - {p})) by XREAL_1:6;
then i + (len (f - {p})) <= (len (f - {p})) + (len (IdFinS (p,(card A)))) by CARD_1:def 7;
then A47: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22;
A48: 1 <= i by A44, FINSEQ_3:25;
then 1 + (len (f - {p})) <= i + (len (f - {p})) by XREAL_1:6;
then A49: i + (len (f - {p})) in seq ((len (f - {p})),(card A)) by A46, CALCUL_2:1;
i <= i + (len (f - {p})) by NAT_1:11;
then 1 <= i + (len (f - {p})) by A48, XXREAL_0:2;
then i + (len (f - {p})) in dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A47, FINSEQ_3:25;
then A50: i + (len (f - {p})) in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by FINSEQ_1:def 3;
a = (Sgm A) . ((i + (len (f - {p}))) - (len (f - {p}))) by A45;
then a = F . (i + (len (f - {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 - {p}) ^ (IdFinS (p,(card A)))) = (len (f - {p})) + (len (IdFinS (p,(card A)))) by FINSEQ_1:22
.= ((len f) - (card A)) + (len (IdFinS (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 - {p}))) \/ (seq ((len (f - {p})),(card A))) by A10, A24, A54, Lm1;

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

assume A58: a1 in Seg (len (f - {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 - {p})),(card A))

assume A62: a2 in seq ((len (f - {p})),(card A)) ; :: thesis: contradiction
then reconsider i = a2 as Nat ;
(Sgm A) . (i - (len (f - {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 - {p})) implies a1 = a2 )

assume A63: a2 in Seg (len (f - {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 - {p})),(card A)) implies a1 = a2 )

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

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

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

end;

(Sgm A) . (i - (len (f - {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 - {p}))

assume a2 in Seg (len (f - {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 - {p}))) \/ (seq ((len (f - {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 - {p}) ^ (IdFinS (p,(card A)))) by A24, FINSEQ_1:def 3 ;

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

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

A80: now :: thesis: ( ex i being Nat st
( i in dom (IdFinS (p,(card A))) & k = (len (f - {p})) + i ) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (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 (p,(card A))) and
A83: k = (len (f - {p})) + i ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k
len (IdFinS (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 - {p})) by A83, XREAL_1:6;
A86: 1 <= i by A82, FINSEQ_3:25;
then 1 + (len (f - {p})) <= k by A83, XREAL_1:6;
then A87: k in seq ((len (f - {p})),(card A)) by A85, CALCUL_2:1;
then F . k = (Sgm A) . (k - (len (f - {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 {p} by FUNCT_1:def 7;
then f . (F . k) = p by TARSKI:def 1;
then (F * f) . k = p by A81, FUNCT_1:12;
then A88: (Per (f,F)) . k = p by CALCUL_2:def 2;
i in Seg (card A) by A86, A84, FINSEQ_1:1;
hence (Per (f,F)) . k = (IdFinS (p,(card A))) . i by A88, FUNCOP_1:7
.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A82, A83, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

assume A89: k in dom (f - {p}) ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k
then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def 3;
k in Seg (len (f - {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 - {p}) . k by FINSEQ_3:def 1
.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A89, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

end;

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

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

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

end;

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

end;