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

ex G being non empty strict binary DTConstrStr st
( the carrier of G = F₁() & ( for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff P₁[x,y,z] ) ) )