let x be Element of TriangularNumbers ; :: thesis: x is triangular
x in TriangularNumbers by SUBSET_1:def 1;
then ex n being Nat st x = Polygon (3,n) ;
hence x is triangular ; :: thesis: verum