set C = DiscreteCat the empty set ;
take DiscreteCat the empty set ; :: thesis: ( DiscreteCat the empty set is strict & DiscreteCat the empty set is empty )
thus ( DiscreteCat the empty set is strict & DiscreteCat the empty set is empty ) by Def16; :: thesis: verum