:: deftheorem defines <=> GRZLOG_1:def 16 :
for t, u being GRZ-formula holds t <=> u = (t => u) '&' (u => t);