reconsider a = 0 as Nat ;
take f = seq_const a; :: thesis: f is triangular-valued
thus f is triangular-valued ; :: thesis: verum