let U0 be with_const_op Universal_Algebra; :: thesis: for H being non empty Subset of (Sub U0) holds meet ((Carr U0) .: H) is non empty Subset of U0
let H be non empty Subset of (Sub U0); :: thesis: meet ((Carr U0) .: H) is non empty Subset of U0
set u = the Element of Constants U0;
reconsider CH = (Carr U0) .: H as Subset-Family of U0 ;
A1: for S being set st S in (Carr U0) .: H holds
the Element of Constants U0 in S

proof

let S be set ; :: thesis: ( S in (Carr U0) .: H implies the Element of Constants U0 in S )
assume A2: S in (Carr U0) .: H ; :: thesis: the Element of Constants U0 in S
then reconsider S = S as Subset of U0 ;
consider X1 being Element of Sub U0 such that
X1 in H and
A3: S = (Carr U0) . X1 by A2, FUNCT_2:65;
reconsider X1 = X1 as strict SubAlgebra of U0 by UNIALG_2:def 14;
S = the carrier of X1 by A3, Def4;
hence the Element of Constants U0 in S by Th11; :: thesis: verum

end;

CH <> {} by Th9;
hence meet ((Carr U0) .: H) is non empty Subset of U0 by A1, SETFAM_1:def 1; :: thesis: verum