let X be set ; :: thesis: for S being Language
for D being RuleSet of S st R0 S in D & X is S -covering & not X is D -inconsistent holds
( X is S -mincover & X is D -expanded )
let S be Language; :: thesis: for D being RuleSet of S st R0 S in D & X is S -covering & not X is D -inconsistent holds
( X is S -mincover & X is D -expanded )
let D be RuleSet of S; :: thesis: ( R0 S in D & X is S -covering & not X is D -inconsistent implies ( X is S -mincover & X is D -expanded ) )
set G0 = R0 S;
set E0 = {(R0 S)};
assume that
B0: R0 S in D and
B1: ( X is S -covering & not X is D -inconsistent ) ; :: thesis: ( X is S -mincover & X is D -expanded )
B2: {(R0 S)} c= D by B0, ZFMISC_1:31;
BBB3: for phi being wff string of S holds
( ( phi in X implies not xnot phi in X ) & ( not phi in X implies xnot phi in X ) )

proof

let phi be wff string of S; :: thesis: ( ( phi in X implies not xnot phi in X ) & ( not phi in X implies xnot phi in X ) )

hereby :: thesis: ( not phi in X implies xnot phi in X )

assume phi in X ; :: thesis: not xnot phi in X
then phi is X,{(R0 S)} -provable by Lm2;
then phi is X,D -provable by B2, Lm35;
then not xnot phi is X,D -provable by B1, DefInc;
then not xnot phi is X,{(R0 S)} -provable by B2, Lm35;
hence not xnot phi in X by Lm2; :: thesis: verum

end;

assume not phi in X ; :: thesis: xnot phi in X
hence xnot phi in X by B1, FOMODEL2:def 40; :: thesis: verum

end;

then for phi being wff string of S holds
( phi in X iff not xnot phi in X ) ;
hence X is S -mincover by FOMODEL2:def 34; :: thesis: X is D -expanded

now

let x be set ; :: thesis: ( x is X,D -provable implies x in X )
assume C0: x is X,D -provable ; :: thesis: x in X
then reconsider phi = x as wff string of S by Lm33;
not xnot phi is X,D -provable by C0, B1, DefInc;
then not xnot phi is X,{(R0 S)} -provable by B2, Lm35;
then not xnot phi in X by Lm2;
hence x in X by BBB3; :: thesis: verum

end;

hence X is D -expanded by DefExpanded2; :: thesis: verum