[:({0} *),{0}:] c= [:({0} *),{0}:] ;
then reconsider DER = [:({0} *),{0}:] as non empty Relation of ({0} *),{0} ;
reconsider EM = typestr(# {0},op2,op2,op2,DER #) as non empty typestr ;
take EM ; :: thesis: EM is SynTypes_Calculus-like
thus for x being type of EM holds <*x*> ==>. x ; :: according to PRELAMB:def 18 :: thesis: ( ( for T being FinSequence of EM
for x, y being type of EM st T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for T being FinSequence of EM
for x, y being type of EM st <*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y, z being type of EM st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds
(X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y being type of EM st X ==>. x & Y ==>. y holds
X ^ Y ==>. x * y ) )
thus ( ( for T being FinSequence of EM
for x, y being type of EM st T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for T being FinSequence of EM
for x, y being type of EM st <*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of EM
for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds
((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y, z being type of EM st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds
(X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM
for x, y being type of EM st X ==>. x & Y ==>. y holds
X ^ Y ==>. x * y ) ) ; :: thesis: verum