consider R being Relation of F₁(),F₂() such that
A1: for x, y being object 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, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) )
thus for x, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) ) by A1; :: thesis: verum