theorem Th29: :: CARDFIL4:34

for i, j, n being Nat st n = max (i,j) holds
square-uparrow n c= (square-uparrow i) /\ (square-uparrow j)