let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) holds

( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p )

let X be Subset of (CQC-WFF Al); :: thesis: ( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p )

thus ( X is Inconsistent implies for p being Element of CQC-WFF Al holds X |- p ) :: thesis: ( ( for p being Element of CQC-WFF Al holds X |- p ) implies X is Inconsistent )

then ( X |- VERUM Al & X |- 'not' (VERUM Al) ) ;

hence X is Inconsistent ; :: thesis: verum

( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p )

let X be Subset of (CQC-WFF Al); :: thesis: ( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p )

thus ( X is Inconsistent implies for p being Element of CQC-WFF Al holds X |- p ) :: thesis: ( ( for p being Element of CQC-WFF Al holds X |- p ) implies X is Inconsistent )

proof

assume
for p being Element of CQC-WFF Al holds X |- p
; :: thesis: X is Inconsistent
assume
X is Inconsistent
; :: thesis: for p being Element of CQC-WFF Al holds X |- p

then consider q being Element of CQC-WFF Al such that

A1: X |- q and

A2: X |- 'not' q ;

consider f2 being FinSequence of CQC-WFF Al such that

A3: rng f2 c= X and

A4: |- f2 ^ <*('not' q)*> by A2;

let p be Element of CQC-WFF Al; :: thesis: X |- p

consider f1 being FinSequence of CQC-WFF Al such that

A5: rng f1 c= X and

A6: |- f1 ^ <*q*> by A1;

take f3 = f1 ^ f2; :: according to HENMODEL:def 1 :: thesis: ( rng f3 c= X & |- f3 ^ <*p*> )

A7: rng f3 = (rng f1) \/ (rng f2) by FINSEQ_1:31;

A8: |- (f1 ^ f2) ^ <*('not' q)*> by A4, CALCUL_2:20;

|- (f1 ^ f2) ^ <*q*> by A6, Th5;

hence ( rng f3 c= X & |- f3 ^ <*p*> ) by A5, A3, A8, A7, CALCUL_2:25, XBOOLE_1:8; :: thesis: verum

end;then consider q being Element of CQC-WFF Al such that

A1: X |- q and

A2: X |- 'not' q ;

consider f2 being FinSequence of CQC-WFF Al such that

A3: rng f2 c= X and

A4: |- f2 ^ <*('not' q)*> by A2;

let p be Element of CQC-WFF Al; :: thesis: X |- p

consider f1 being FinSequence of CQC-WFF Al such that

A5: rng f1 c= X and

A6: |- f1 ^ <*q*> by A1;

take f3 = f1 ^ f2; :: according to HENMODEL:def 1 :: thesis: ( rng f3 c= X & |- f3 ^ <*p*> )

A7: rng f3 = (rng f1) \/ (rng f2) by FINSEQ_1:31;

A8: |- (f1 ^ f2) ^ <*('not' q)*> by A4, CALCUL_2:20;

|- (f1 ^ f2) ^ <*q*> by A6, Th5;

hence ( rng f3 c= X & |- f3 ^ <*p*> ) by A5, A3, A8, A7, CALCUL_2:25, XBOOLE_1:8; :: thesis: verum

then ( X |- VERUM Al & X |- 'not' (VERUM Al) ) ;

hence X is Inconsistent ; :: thesis: verum