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