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 ; :: thesis: for x, y being Element of N holds
( x <= y iff P1[x,y] )
let x, y be Element of N; :: thesis: ( 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; :: thesis: verum