reconsider a = Triangle 1 as Nat by TARSKI:1;
take a ; :: thesis: ( a is triangular & a is square & not a is zero )
1 = 1 ^2 ;
then ( Triangle 1 is triangular & Triangle 1 is square ) by FINSEQ_2:50, RVSUM_1:73;
hence ( a is triangular & a is square & not a is zero ) ; :: thesis: verum