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 and
A2: X |- 'not' p by Def3;
consider f1 being FinSequence of CQC-WFF such that
A3: rng f1 c= X and
A4: |- f1 ^ <*p*> by A1, Def2;
consider f2 being FinSequence of CQC-WFF such that
A5: rng f2 c= X and
A6: |- f2 ^ <*('not' p)*> by A2, Def2;
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 A3, A5, XBOOLE_1:8; :: thesis: ( Y is finite & not Y is Consistent )
|- (f1 ^ f2) ^ <*('not' p)*> by A6, CALCUL_2:20;
then A7: Y |- 'not' p by Def2;
|- (f1 ^ f2) ^ <*p*> by A4, Th5;
then Y |- p by Def2;
hence ( Y is finite & not Y is Consistent ) by A7, Def3; :: thesis: verum