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