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 ) )

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

( 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 that 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;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

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