theorem :: CARDFIL4:31

for n being Nat holds square-uparrow n c= [:NAT,NAT:] \ [:(Segm n),(Segm n):]