take 1Cat ({},{}) ; :: thesis: 1Cat ({},{}) is discrete
thus 1Cat ({},{}) is discrete ; :: thesis: verum