:: deftheorem defines DualSet ZMODLAT3:def 6 :
for L being Z_Lattice holds DualSet L = { v where v is Dual of L : verum } ;