:: deftheorem defines ExWALattice LATWAL_2:def 16 :
ExWALattice = LattStr(# {0,1,2,3,4},ex1234\/,ex1234/\ #);