reconsider a = Triangle 1 as number by TARSKI:1;
take a ; :: thesis: ( a is triangular & not a is zero )
thus ( a is triangular & not a is zero ) ; :: thesis: verum