let X be set ; :: thesis: for S being Language
for D being RuleSet of S st R#0 S in D & X is S -covering & X is D -consistent holds
( X is S -mincover & X is D -expanded )
let S be Language; :: thesis: for D being RuleSet of S st R#0 S in D & X is S -covering & X is D -consistent holds
( X is S -mincover & X is D -expanded )
let D be RuleSet of S; :: thesis: ( R#0 S in D & X is S -covering & X is D -consistent implies ( X is S -mincover & X is D -expanded ) )
set G0 = R#0 S;
set E0 = {(R#0 S)};
assume that
A1: R#0 S in D and
A2: ( X is S -covering & X is D -consistent ) ; :: thesis: ( X is S -mincover & X is D -expanded )
A3: {(R#0 S)} c= D by A1, ZFMISC_1:31;
A4: 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,{(R#0 S)} -provable by Th6;
then phi is X,D -provable by A3, Lm19;
then not xnot phi is X,D -provable by A2;
then not xnot phi is X,{(R#0 S)} -provable by A3, Lm19;
hence not xnot phi in X by Th6; :: thesis: verum

end;

assume not phi in X ; :: thesis: xnot phi in X
hence xnot phi in X by A2; :: 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 ; :: thesis: X is D -expanded

now :: thesis: for x being set st x is X,D -provable holds
x in X

let x be set ; :: thesis: ( x is X,D -provable implies x in X )
assume A5: x is X,D -provable ; :: thesis: x in X
then reconsider phi = x as wff string of S by Lm25;
not xnot phi is X,D -provable by A5, A2;
then not xnot phi is X,{(R#0 S)} -provable by A3, Lm19;
then not xnot phi in X by Th6;
hence x in X by A4; :: thesis: verum

end;

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