consider R being Relation of F_{1}(),F_{2}() such that

A1: for x, y being object holds

( [x,y] in R iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )
from RELSET_1:sch 1();

take R ; :: thesis: for x, y being set holds

( [x,y] in R iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )

thus for x, y being set holds

( [x,y] in R iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )
by A1; :: thesis: verum

A1: for x, y being object holds

( [x,y] in R iff ( x in F

take R ; :: thesis: for x, y being set holds

( [x,y] in R iff ( x in F

thus for x, y being set holds

( [x,y] in R iff ( x in F