let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) st X is Inconsistent holds
ex Y being Subset of (CQC-WFF Al) st
( Y c= X & Y is finite & Y is Inconsistent )
let X be Subset of (CQC-WFF Al); :: thesis: ( X is Inconsistent implies ex Y being Subset of (CQC-WFF Al) st
( Y c= X & Y is finite & Y is Inconsistent ) )
assume X is Inconsistent ; :: thesis: ex Y being Subset of (CQC-WFF Al) st
( Y c= X & Y is finite & Y is Inconsistent )
then consider p being Element of CQC-WFF Al such that
A1: X |- p and
A2: X |- 'not' p ;
consider f1 being FinSequence of CQC-WFF Al such that
A3: rng f1 c= X and
A4: |- f1 ^ <*p*> by A1;
consider f2 being FinSequence of CQC-WFF Al such that
A5: rng f2 c= X and
A6: |- f2 ^ <*('not' p)*> by A2;
reconsider Y = rng (f1 ^ f2) as Subset of (CQC-WFF Al) ;
take Y ; :: thesis: ( Y c= X & Y is finite & Y is Inconsistent )
Y = (rng f1) \/ (rng f2) by FINSEQ_1:31;
hence Y c= X by A3, A5, XBOOLE_1:8; :: thesis: ( Y is finite & Y is Inconsistent )
|- (f1 ^ f2) ^ <*('not' p)*> by A6, CALCUL_2:20;
then A7: Y |- 'not' p ;
|- (f1 ^ f2) ^ <*p*> by A4, Th5;
then Y |- p ;
hence ( Y is finite & Y is Inconsistent ) by A7; :: thesis: verum