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