:: deftheorem defines SetBelow WAYBEL35:def 8 :
for R being Relation
for C being set
for y being object holds SetBelow (R,C,y) = (R " {y}) /\ C;