:: deftheorem defines [#] HILB10_7:def 1 :
for X being finite set holds [#] X = X;