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