let F, G be Subset of PL-WFF; :: thesis: ( F c= G & not F is consistent implies not G is consistent )
assume A2: ( F c= G & not F is consistent ) ; :: thesis: not G is consistent
then consider p being Element of PL-WFF such that
A1: ( F |- p & F |- 'not' p ) ;
( G |- p & G |- 'not' p ) by monmp, A1, A2;
hence not G is consistent ; :: thesis: verum