scheme :: YELLOW_0:sch 1
RelStrEx{ F1() -> non empty set , P1[ set , set ] } :
ex L being non empty strict RelStr st
( the carrier of L = F1() & ( for a, b being Element of L holds
( a <= b iff P1[a,b] ) ) )