:: deftheorem defines maximally-consistent PROOFS_1:def 30 :
for P being non empty ProofSystem
for B being Subset of P holds
( B is maximally-consistent iff ( B is consistent & ( for B1 being Subset of P st B c< B1 holds
B1 is inconsistent ) ) );