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

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