let F be Subset of PL-WFF; :: thesis: ( not F is consistent implies ex G being Subset of PL-WFF st
( G is finite & not G is consistent & G c= F ) )
assume not F is consistent ; :: thesis: ex G being Subset of PL-WFF st
( G is finite & not G is consistent & G c= F )
then consider A being Element of PL-WFF such that
A1: ( F |- A & F |- 'not' A ) ;
consider G being Subset of PL-WFF such that
A2: ( G c= F & G is finite & G |- A ) by exfin, A1;
consider H being Subset of PL-WFF such that
A2a: ( H c= F & H is finite & H |- 'not' A ) by exfin, A1;
A5: G \/ H |- A by A2, monmp, XBOOLE_1:11;
G \/ H |- 'not' A by A2a, XBOOLE_1:11, monmp;
then not G \/ H is consistent by A5;
hence ex G being Subset of PL-WFF st
( G is finite & not G is consistent & G c= F ) by XBOOLE_1:8, A2, A2a; :: thesis: verum