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 being Element of F_{1}()

for y being Element of F_{2}() holds

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

thus for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in R iff 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 being Element of F

for y being Element of F

( [x,y] in R iff P

thus for x being Element of F

for y being Element of F

( [x,y] in R iff P