:: deftheorem defines <==>. PRELAMB:def 19 :
for s being SynTypes_Calculus
for x, y being type of s holds
( x <==>. y iff ( <*x*> ==>. y & <*y*> ==>. x ) );