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 )
proof
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 ^ <*()*> 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) ^ <*()*> by ;
|- (f1 ^ f2) ^ <*q*> by ;
hence ( rng f3 c= X & |- f3 ^ <*p*> ) by ; :: thesis: verum
end;
assume for p being Element of CQC-WFF Al holds X |- p ; :: thesis: X is Inconsistent
then ( X |- VERUM Al & X |- 'not' (VERUM Al) ) ;
hence X is Inconsistent ; :: thesis: verum