:: deftheorem defines QLTLattice1 LATQUASI:def 8 :
QLTLattice1 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);