theorem :: NECKLA_3:32

for G being irreflexive RelStr st G in fin_RelStr_sp holds
ComplRelStr G in fin_RelStr_sp