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

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