let m, n be Nat; ( m = n - 1 implies square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):] )
assume A1:
m = n - 1
; square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):]
let x be object ; TARSKI:def 3 ( not x in square-uparrow n or x in [:NAT,NAT:] \ [:(Seg m),(Seg m):] )
assume A2:
x in square-uparrow n
; 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):]
hence
x in [:NAT,NAT:] \ [:(Seg m),(Seg m):]
by A2, XBOOLE_0:def 5; verum