reconsider m = n - 1 as Nat by CHORD:1;
( 0 < n & n - 1 < n - 0 )
by XREAL_1:15;
then
( 0 in Segm n & m in Segm n )
by NAT_1:44;
then
( 0 in n & m in n )
by ORDINAL1:def 17;
then
( {[m,0]} is n -valued & {[m,0]} is n -defined )
by RELSET_1:3;
hence
(addRel (n,1)) \/ {[(n - 1),0]} is Relation of n
by EXCHSORT:83; verum