:: deftheorem defines consistent PROOFS_1:def 19 :
for P being non empty ProofSystem holds
( P is consistent iff ex a being object st
( a in P & not P |- a ) );