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 ^ <*('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;
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