take IdCat the Category ; :: thesis: ( IdCat the Category is strict & IdCat the Category is discrete )
thus ( IdCat the Category is strict & IdCat the Category is discrete ) ; :: thesis: verum