consider m' being Nat such that
A1: m = m' ^2 by Def3;
A2: not m' is even by A1;
consider n' being Nat such that
A3: n = n' ^2 by Def3;
A4: not n' is even by A3;
reconsider m'' = m as Element of NAT by ORDINAL1:def 13;
reconsider n'' = n as Element of NAT by ORDINAL1:def 13;
A5: (m'' + n'') mod 4 = ((m'' mod 4) + (n'' mod 4)) mod 4 by EULER_2:8
.= (1 + (n'' 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 mn' being Nat such that
A6: m + n = mn' ^2 by Def3;
mn' is even by A6;
hence contradiction by A5, A6, Th3; :: thesis: verum

end;