let x be Nat; :: thesis: ( x is triangular implies x is 3 -gonal )
assume x is triangular ; :: thesis: x is 3 -gonal
then consider n being Nat such that
A1: x = Triangle n ;
x = Polygon (3,n) by A1, Th40;
hence x is 3 -gonal ; :: thesis: verum