consider X being Pythagorean_triple such that
A1: ( not X is degenerate & X is simplified ) and
4 * 1 in X by Th14;
take X ; :: thesis: ( not X is degenerate & X is simplified )
thus ( not X is degenerate & X is simplified ) by A1; :: thesis: verum