let n, i, j be Nat; :: thesis: ( ( [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):] ) ; :: thesis: ((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; :: thesis: verum