:: deftheorem defines -provable PROOFS_1:def 11 :
for B being set
for R being Rule
for a being object holds
( a is B,R -provable iff B,R |- a );