theorem Th26: :: CARDFIL4:29

for n being Nat
for no being Element of OrderedNAT st no = n holds
square-uparrow n = [:(uparrow no),(uparrow no):]