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

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