:: deftheorem defines Normal_forms_on NORMFORM:def 9 :
for A being set holds Normal_forms_on A = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ;