set C = DiscreteCat the empty set ;
take DiscreteCat the empty set ; :: thesis: DiscreteCat the empty set is strict
thus DiscreteCat the empty set is strict ; :: thesis: verum