theorem Th25: :: CARDFIL4:26

for n being Nat holds [n,n] in square-uparrow n