consider r being Relation of F_{1}() such that

A1: for x, y being Element of F_{1}() holds

( [x,y] in r iff P_{1}[x,y] )
from RELSET_1:sch 2();

take X = ARS(# F_{1}(),r #); :: thesis: ( the carrier of X = F_{1}() & ( for x, y being Element of X holds

( x ==> y iff P_{1}[x,y] ) ) )

thus the carrier of X = F_{1}()
; :: thesis: for x, y being Element of X holds

( x ==> y iff P_{1}[x,y] )

thus for x, y being Element of X holds

( x ==> y iff P_{1}[x,y] )
by A1; :: thesis: verum

A1: for x, y being Element of F

( [x,y] in r iff P

take X = ARS(# F

( x ==> y iff P

thus the carrier of X = F

( x ==> y iff P

thus for x, y being Element of X holds

( x ==> y iff P