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 ;
per cases ( (sqrt 2) ^ (sqrt 2) is rational or (sqrt 2) ^ (sqrt 2) is irrational ) ;
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 )
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;
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 )
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;
end;