theorem :: PARTFUN2:33

for C, D being non empty set
for SC being Subset of C
for d being Element of D st SC --> d is total holds
SC <> {}