theorem :: CARDFIL4:30

for m, n being Nat st m = n - 1 holds
square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):]