let X be set ; 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; 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 ; ( [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; verum