theorem Th15: :: WAYBEL35:15

for R being Relation
for C, x, y being set holds
( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )