:: deftheorem Def28 defines -closed PROOFS_1:def 31 :
for R being Rule
for X being set holds
( X is R -closed iff for Y being set
for a being object st [Y,a] in R & Y c= X holds
a in X );