reconsider n99 = n as Element of NAT by ORDINAL1:def 12;
reconsider m99 = m as Element of NAT by ORDINAL1:def 12;
consider m9 being Nat such that
A1: m = m9 ^2 by Def3;
A2: m9 is odd by A1;
consider n9 being Nat such that
A3: n = n9 ^2 by Def3;
A4: n9 is odd by A3;
A5: (m99 + n99) mod 4 = ((m99 mod 4) + (n99 mod 4)) mod 4 by NAT_D:66
.= (1 + (n99 mod 4)) mod 4 by A1, A2, Th4
.= (1 + 1) mod 4 by A3, A4, Th4
.= 2 by NAT_D:24 ;

hereby :: thesis: verum

assume m + n is square ; :: thesis: contradiction
then consider mn9 being Nat such that
A6: m + n = mn9 ^2 ;
mn9 is even by A6;
hence contradiction by A5, A6, Th3; :: thesis: verum

end;