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