let X be set ; :: thesis: for R being Relation
for x, y being set holds
( [x,y] in R |_2 X iff ( x in X & y in X & [x,y] in R ) )
let R be Relation; :: thesis: for x, y being set holds
( [x,y] in R |_2 X iff ( x in X & y in X & [x,y] in R ) )
let x, y be set ; :: thesis: ( [x,y] in R |_2 X iff ( x in X & y in X & [x,y] in R ) )
R |_2 X = X |` (R | X) by WELLORD1:11;
then ( [x,y] in R |_2 X iff ( y in X & [x,y] in R | X ) ) by RELAT_1:def 12;
hence ( [x,y] in R |_2 X iff ( x in X & y in X & [x,y] in R ) ) by RELAT_1:def 11; :: thesis: verum