let Y be set ; :: thesis: for S being Language
for D being RuleSet of S
for X being Subset of Y st X is D -inconsistent holds
Y is D -inconsistent
let S be Language; :: thesis: for D being RuleSet of S
for X being Subset of Y st X is D -inconsistent holds
Y is D -inconsistent
let D be RuleSet of S; :: thesis: for X being Subset of Y st X is D -inconsistent holds
Y is D -inconsistent
let X be Subset of Y; :: thesis: ( X is D -inconsistent implies Y is D -inconsistent )
set N = TheNorSymbOf S;
assume X is D -inconsistent ; :: thesis: Y is D -inconsistent
then consider phi1, phi2 being wff string of S such that
B0: ( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) by DefInc;
thus Y is D -inconsistent by DefInc, B0; :: thesis: verum