consider X being Pythagorean_triple such that
A1: ( not X is degenerate & X is simplified & 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