:: deftheorem defines |- PROOFS_1:def 17 :
for P being ProofSystem
for a being object holds
( P |- a iff the Axioms of P, the Rules of P |- a );