:: deftheorem defines -provable PROOFS_1:def 16 :
for B being set
for R being Rule
for a being object holds
( a is B,R -provable iff for C being Extension of B
for E being Extension of R holds C,E |- a );