:: deftheorem defines Ordset GROUP_18:def 1 :
for G being finite Group holds Ordset G = { (ord a) where a is Element of G : verum } ;