let U0 be Universal_Algebra; :: thesis: for H being non empty Subset of (Sub U0) holds not (Carr U0) .: H is empty
let H be non empty Subset of (Sub U0); :: thesis: not (Carr U0) .: H is empty
consider u being Element of Sub U0 such that
A1: u in H by SUBSET_1:4;
(Carr U0) . u in (Carr U0) .: H by A1, FUNCT_2:35;
hence not (Carr U0) .: H is empty ; :: thesis: verum