:: deftheorem Def30r defines Theorems PROOFS_1:def 34 :
for X being set
for R being Rule
for b₃ being set holds
( b₃ = Theorems (X,R) iff for a being object holds
( a in b₃ iff X,R |- a ) );