consider R being Relation of F₁() such that
A1: for a, b being Element of F₁() holds
( [a,b] in R iff P₁[a,b] ) from RELSET_1:sch 2();
take L = RelStr(# F₁(),R #); :: thesis: ( the carrier of L = F₁() & ( for a, b being Element of L holds
( a <= b iff P₁[a,b] ) ) )
thus the carrier of L = F₁() ; :: thesis: for a, b being Element of L holds
( a <= b iff P₁[a,b] )
let a, b be Element of L; :: thesis: ( a <= b iff P₁[a,b] )
( a <= b iff [a,b] in R ) by ORDERS_2:def 9;
hence ( a <= b iff P₁[a,b] ) by A1; :: thesis: verum