:: deftheorem defines TernaryFieldEx ALGSTR_3:def 3 :
TernaryFieldEx = TernaryFieldStr(# REAL,(In (0,REAL)),(In (1,REAL)),ternaryreal #);