reconsider I = {} as Relation of n,n by RELSET_1:12;
take RelStr(# n,I #) ; :: thesis: the carrier of RelStr(# n,I #) = n
thus the carrier of RelStr(# n,I #) = n ; :: thesis: verum