consider R being Relation of the carrier of F1() such that
A1:
for x, y being Element of F1() holds
( [x,y] in R iff P1[x,y] )
from RELSET_1:sch 2();
set N = RelMonoid(# the carrier of F1(), the multF of F1(), the OneF of F1(),R #);
multLoopStr(# the carrier of RelMonoid(# the carrier of F1(), the multF of F1(), the OneF of F1(),R #), the multF of RelMonoid(# the carrier of F1(), the multF of F1(), the OneF of F1(),R #), the OneF of RelMonoid(# the carrier of F1(), the multF of F1(), the OneF of F1(),R #) #) = multLoopStr(# the carrier of F1(), the multF of F1(), the OneF of F1() #)
;
then reconsider N = RelMonoid(# the carrier of F1(), the multF of F1(), the OneF of F1(),R #) as strict RelExtension of F1() by RE;
take
N
; for x, y being Element of N holds
( x <= y iff P1[x,y] )
let x, y be Element of N; ( x <= y iff P1[x,y] )
( [x,y] in R iff P1[x,y] )
by A1;
hence
( x <= y iff P1[x,y] )
by ORDERS_2:def 5; verum