let k be Nat; :: thesis: for p being Prime st p = (4 * k) + 1 holds
ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )
let p be Prime; :: thesis: ( p = (4 * k) + 1 implies ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) ) )
assume A1: p = (4 * k) + 1 ; :: thesis: ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )
then p mod 4 = 1 by Lm6, NAT_D:21;
then consider a, b being Nat such that
A2: p = (a ^2) + (b ^2) by NAT_5:23;

now :: thesis: not 0 >= a

assume 0 >= a ; :: thesis: contradiction
then a = 0 ;
hence contradiction by A2; :: thesis: verum

end;

then reconsider a = a as positive Nat ;

now :: thesis: not 0 >= b

assume 0 >= b ; :: thesis: contradiction
then b = 0 ;
hence contradiction by A2; :: thesis: verum

end;

then reconsider b = b as positive Nat ;
a <> b

proof

assume a = b ; :: thesis: contradiction
then A3: p = 2 * (a ^2) by A2;
p = (2 * (2 * k)) + 1 by A1;
hence contradiction by A3; :: thesis: verum

end;

per cases then ( a < b or a > b ) by XXREAL_0:1;

suppose A4: a < b ; :: thesis: ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )

take b ; :: thesis: ex b being positive Nat st
( b > b & p = (b ^2) + (b ^2) )
take a ; :: thesis: ( b > a & p = (b ^2) + (a ^2) )
thus ( b > a & p = (b ^2) + (a ^2) ) by A2, A4; :: thesis: verum

end;

suppose A5: a > b ; :: thesis: ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )

take a ; :: thesis: ex b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )
take b ; :: thesis: ( a > b & p = (a ^2) + (b ^2) )
thus ( a > b & p = (a ^2) + (b ^2) ) by A2, A5; :: thesis: verum

end;

end;