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