scheme :: YELLOW_0:sch 1
RelStrEx{ F₁() -> non empty set , P₁[ set , set ] } :

ex L being non empty strict RelStr st
( the carrier of L = F₁() & ( for a, b being Element of L holds
( a <= b iff P₁[a,b] ) ) )