let n, i, j be Nat; ( ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) implies ((j - i) mod n) + 1 in Seg n )
assume
( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] )
; ((j - i) mod n) + 1 in Seg n
then
( i in Seg n & j in Seg n )
by ZFMISC_1:87;
hence
((j - i) mod n) + 1 in Seg n
by Lm2; verum