for L being RelStr
for AR being Relation of L st AR is satisfying_SI holds
AR is satisfying_INT