take TriangularFS (0,1,2) ; :: thesis: TriangularFS (0,1,2) is triangular
thus TriangularFS (0,1,2) is triangular ; :: thesis: verum