consider R being Relation 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 RELAT_1:sch 1();

R c= [:F_{1}(),F_{2}():]
_{1}(),F_{2}() ;

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

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

thus for x, y being object 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

R c= [:F

proof

then reconsider R = R as Relation of F
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in R or [x1,x2] in [:F_{1}(),F_{2}():] )

assume [x1,x2] in R ; :: thesis: [x1,x2] in [:F_{1}(),F_{2}():]

then ( x1 in F_{1}() & x2 in F_{2}() )
by A1;

hence [x1,x2] in [:F_{1}(),F_{2}():]
by ZFMISC_1:87; :: thesis: verum

end;assume [x1,x2] in R ; :: thesis: [x1,x2] in [:F

then ( x1 in F

hence [x1,x2] in [:F

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

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

thus for x, y being object holds

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