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
consider u being Element of Constants U0;
A1: for S being set st S in (Carr U0) .: H holds
u in S

proof

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

end;

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