scheme :: DTCONSTR:sch 1
DTConstrStrEx{ F1() -> non empty set , P1[ object , object ] } :
ex G being non empty strict DTConstrStr st
( the carrier of G = F1() & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff P1[x,p] ) ) )