for U0 being Universal_Algebra
for H being non empty Subset of (Sub U0) holds not (Carr U0) .: H is empty