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

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