let m, n be Nat; :: thesis: ( m = n - 1 implies square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):] )

assume A1: m = n - 1 ; :: thesis: square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):]

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-uparrow n or x in [:NAT,NAT:] \ [:(Seg m),(Seg m):] )

assume A2: x in square-uparrow n ; :: thesis: x in [:NAT,NAT:] \ [:(Seg m),(Seg m):]

then reconsider y = x as Element of [:NAT,NAT:] ;

consider n1, n2 being Nat such that

A3: n1 = y `1 and

A4: n2 = y `2 and

A5: n <= n1 and

n <= n2 by A2, Def3;

not x in [:(Seg m),(Seg m):]

assume A1: m = n - 1 ; :: thesis: square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):]

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-uparrow n or x in [:NAT,NAT:] \ [:(Seg m),(Seg m):] )

assume A2: x in square-uparrow n ; :: thesis: x in [:NAT,NAT:] \ [:(Seg m),(Seg m):]

then reconsider y = x as Element of [:NAT,NAT:] ;

consider n1, n2 being Nat such that

A3: n1 = y `1 and

A4: n2 = y `2 and

A5: n <= n1 and

n <= n2 by A2, Def3;

not x in [:(Seg m),(Seg m):]

proof

hence
x in [:NAT,NAT:] \ [:(Seg m),(Seg m):]
by A2, XBOOLE_0:def 5; :: thesis: verum
assume
x in [:(Seg m),(Seg m):]
; :: thesis: contradiction

then ex x1, x2 being object st

( x1 in Seg m & x2 in Seg m & x = [x1,x2] ) by ZFMISC_1:def 2;

then ( n1 <= m & n2 <= m ) by A3, A4, FINSEQ_1:1;

then n <= m by A5, XXREAL_0:2;

then n - n <= (n - 1) - n by A1, XREAL_1:9;

then 0 <= - 1 ;

hence contradiction ; :: thesis: verum

end;then ex x1, x2 being object st

( x1 in Seg m & x2 in Seg m & x = [x1,x2] ) by ZFMISC_1:def 2;

then ( n1 <= m & n2 <= m ) by A3, A4, FINSEQ_1:1;

then n <= m by A5, XXREAL_0:2;

then n - n <= (n - 1) - n by A1, XREAL_1:9;

then 0 <= - 1 ;

hence contradiction ; :: thesis: verum