:: deftheorem defines Theorems PROOFS_1:def 33 :
for X being set
for R being Rule holds Theorems (X,R) = { t where t is Element of X \/ (rng R) : X,R |- t } ;