:: deftheorem defines Theorem PROOFS_1:def 32 :
for D being non empty set
for R being Rule
for b₃ being Formula holds
( b₃ is Theorem of D,R iff D,R |- b₃ );