consider r being Relation of F₁() such that
A1: for x, y being Element of F₁() holds
( [x,y] in r iff P₁[x,y] ) from RELSET_1:sch 2();
take X = ARS(# F₁(),r #); :: thesis: ( the carrier of X = F₁() & ( for x, y being Element of X holds
( x ==> y iff P₁[x,y] ) ) )
thus the carrier of X = F₁() ; :: thesis: for x, y being Element of X holds
( x ==> y iff P₁[x,y] )
thus for x, y being Element of X holds
( x ==> y iff P₁[x,y] ) by A1; :: thesis: verum