theorem Th27: :: CARDFIL4:32

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