:: deftheorem defines new_set LATTICE5:def 9 :
for A being set holds new_set A = A \/ {{A},{{A}},{{{A}}}};