reconsider a = a as Nat ;
consider m being Nat such that
A0: m ^2 = a by PYTHTRIP:def 3;
thus sqrt a is natural by A0, SQUARE_1:def 2; :: thesis: verum