let R be Relation; :: thesis: for C, x, y being set holds
( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )
let C, x, y be set ; :: thesis: ( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )

hereby :: thesis: ( [x,y] in R & x in C implies x in SetBelow (R,C,y) )

assume A1: x in SetBelow (R,C,y) ; :: thesis: ( [x,y] in R & x in C )
then x in R " {y} by XBOOLE_0:def 4;
then ex a being object st
( [x,a] in R & a in {y} ) by RELAT_1:def 14;
hence [x,y] in R by TARSKI:def 1; :: thesis: x in C
thus x in C by A1, XBOOLE_0:def 4; :: thesis: verum

end;

assume that
A2: [x,y] in R and
A3: x in C ; :: thesis: x in SetBelow (R,C,y)
y in {y} by TARSKI:def 1;
then x in R " {y} by A2, RELAT_1:def 14;
hence x in SetBelow (R,C,y) by A3, XBOOLE_0:def 4; :: thesis: verum