thus ex G being non empty strict DTConstrStr st
( the carrier of G = {0,1} & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff S₁[x,p] ) ) ) from DTCONSTR:sch 1(); :: thesis: verum