let q, s, t be Prime; :: thesis: ( not q ^2 = (s ^2) + (t ^2) or ( s is even & t is odd ) or ( s is odd & t is even ) )
assume A1: q ^2 = (s ^2) + (t ^2) ; :: thesis: ( ( s is even & t is odd ) or ( s is odd & t is even ) )
assume ( s is odd or t is even ) ; :: thesis: ( s is odd & t is even )

per cases then ( s is odd or t is even ) ;

suppose A2: s is odd ; :: thesis: ( s is odd & t is even )

now :: thesis: not t is odd

assume A3: t is odd ; :: thesis: contradiction
then q is even by A1, A2;
then A4: q = 2 by LAGRA4SQ:13;
( 9 <= s ^2 & 9 <= t ^2 ) by A2, A3, Lm4;
then 9 + 9 <= (s ^2) + (t ^2) by XREAL_1:7;
hence contradiction by A1, A4; :: thesis: verum

end;

hence ( s is odd & t is even ) by A2; :: thesis: verum

end;

suppose t is even ; :: thesis: ( s is odd & t is even )

then t = 2 by LAGRA4SQ:13;
then (q ^2) - (s ^2) = 4 by A1;
hence ( s is odd & t is even ) by Th35; :: thesis: verum

end;

end;