:: deftheorem defines component NECKLA_3:def 3 :
for R being RelStr
for x being Element of R holds component x = Class ((EqCl the InternalRel of R),x);