set w = sqrt 2;

A1: ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) = (sqrt 2) ^ ((sqrt 2) ^2) by POWER:33, SQUARE_1:19

.= (sqrt 2) ^ 2 by SQUARE_1:def 2

.= (sqrt 2) ^2 by POWER:46

.= 2 by SQUARE_1:def 2 ;

reconsider dwa = 2 as Real ;

A1: ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) = (sqrt 2) ^ ((sqrt 2) ^2) by POWER:33, SQUARE_1:19

.= (sqrt 2) ^ 2 by SQUARE_1:def 2

.= (sqrt 2) ^2 by POWER:46

.= 2 by SQUARE_1:def 2 ;

reconsider dwa = 2 as Real ;

per cases
( (sqrt 2) ^ (sqrt 2) is rational or (sqrt 2) ^ (sqrt 2) is irrational )
;

end;

suppose A2:
(sqrt 2) ^ (sqrt 2) is rational
; :: thesis: ex x, y being Real st

( x is irrational & y is irrational & x ^ y is rational )

( x is irrational & y is irrational & x ^ y is rational )

take
sqrt 2
; :: thesis: ex y being Real st

( sqrt 2 is irrational & y is irrational & (sqrt 2) ^ y is rational )

take sqrt 2 ; :: thesis: ( sqrt 2 is irrational & sqrt 2 is irrational & (sqrt 2) ^ (sqrt 2) is rational )

thus ( sqrt 2 is irrational & sqrt 2 is irrational & (sqrt 2) ^ (sqrt 2) is rational ) by A2, Th1, INT_2:28; :: thesis: verum

end;( sqrt 2 is irrational & y is irrational & (sqrt 2) ^ y is rational )

take sqrt 2 ; :: thesis: ( sqrt 2 is irrational & sqrt 2 is irrational & (sqrt 2) ^ (sqrt 2) is rational )

thus ( sqrt 2 is irrational & sqrt 2 is irrational & (sqrt 2) ^ (sqrt 2) is rational ) by A2, Th1, INT_2:28; :: thesis: verum

suppose A3:
(sqrt 2) ^ (sqrt 2) is irrational
; :: thesis: ex x, y being Real st

( x is irrational & y is irrational & x ^ y is rational )

( x is irrational & y is irrational & x ^ y is rational )

take
(sqrt 2) ^ (sqrt 2)
; :: thesis: ex y being Real st

( (sqrt 2) ^ (sqrt 2) is irrational & y is irrational & ((sqrt 2) ^ (sqrt 2)) ^ y is rational )

take sqrt 2 ; :: thesis: ( (sqrt 2) ^ (sqrt 2) is irrational & sqrt 2 is irrational & ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) is rational )

thus ( (sqrt 2) ^ (sqrt 2) is irrational & sqrt 2 is irrational & ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) is rational ) by A1, A3, Th1, INT_2:28; :: thesis: verum

end;( (sqrt 2) ^ (sqrt 2) is irrational & y is irrational & ((sqrt 2) ^ (sqrt 2)) ^ y is rational )

take sqrt 2 ; :: thesis: ( (sqrt 2) ^ (sqrt 2) is irrational & sqrt 2 is irrational & ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) is rational )

thus ( (sqrt 2) ^ (sqrt 2) is irrational & sqrt 2 is irrational & ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) is rational ) by A1, A3, Th1, INT_2:28; :: thesis: verum