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