:: deftheorem defines new_set2 LATTICE8:def 3 :
for A being set holds new_set2 A = A \/ {{A},{{A}}};