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

hence meet ((Carr U0) .: H) is non empty Subset of U0 by A1, SETFAM_1:def 1; :: thesis: verum

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

CH <> {}
by Th9;
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;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

hence meet ((Carr U0) .: H) is non empty Subset of U0 by A1, SETFAM_1:def 1; :: thesis: verum