:: deftheorem defines -inconsistent FOMODEL4:def 15 :
for S being Language
for D being RuleSet of S
for X being set holds
( X is D -inconsistent iff ex phi1, phi2 being wff string of S st
( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) );