:: deftheorem defines |- PROOFS_1:def 18 :
for P being non empty ProofSystem
for B being Subset of P holds
( P |- B iff for a being object st a in B holds
P |- a );