take {} T ; :: thesis: {} T is 1st_class
thus {} T is 1st_class ; :: thesis: verum