reconsider I = {} as Relation of n,n by RELSET_1:12;
set R = RelStr(# n,I #);
reconsider R = RelStr(# n,I #) as NatRelStr of n by Def7;
R is irreflexive ;
hence ex b₁ being NatRelStr of n st b₁ is irreflexive ; :: thesis: verum