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