consider R being Relation of F1(),F2() such that
A1:
for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
from RELSET_1:sch 1();
take
R
; :: thesis: for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R iff P1[x,y] )
thus
for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R iff P1[x,y] )
by A1; :: thesis: verum