:: deftheorem Def4 defines well-conjugated CAYLDICK:def 4 :
for N being non empty ConjNormAlgStr holds
( N is well-conjugated iff for a being Element of N holds a is well-conjugated );