let U0 be with_const_op Universal_Algebra; :: thesis: for H being non empty Subset of holds meet ((Carr U0) .: H) is non empty Subset of
let H be non empty Subset of ; :: thesis: meet ((Carr U0) .: H) is non empty Subset of
consider u being Element of Constants U0;
reconsider CH = (Carr U0) .: H as Subset-Family of ;
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 ;
consider X1 being Element of Sub U0 such that
X1 in H and
A3: 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;

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