:: deftheorem Def2 defines [ HEYTING1:def 2 :
for A being set st not A is empty holds
[A] = A;