let U0 be with_const_op Universal_Algebra; :: thesis: for H being non empty Subset of (Sub U0)
for S being non empty Subset of U0 st S = meet ((Carr U0) .: H) holds
S is opers_closed
let H be non empty Subset of (Sub U0); :: thesis: for S being non empty Subset of U0 st S = meet ((Carr U0) .: H) holds
S is opers_closed
let S be non empty Subset of U0; :: thesis: ( S = meet ((Carr U0) .: H) implies S is opers_closed )
assume A1: S = meet ((Carr U0) .: H) ; :: thesis: S is opers_closed
A2: (Carr U0) .: H <> {} by Th9;
for o being operation of U0 holds S is_closed_on o
proof
let o be operation of U0; :: thesis: S is_closed_on o
let s be FinSequence of S; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o or o . s in S )
assume A3: len s = arity o ; :: thesis: o . s in S
now :: thesis: for a being set st a in (Carr U0) .: H holds
o . s in a
let a be set ; :: thesis: ( a in (Carr U0) .: H implies o . s in a )
assume A4: a in (Carr U0) .: H ; :: thesis: o . s in a
then reconsider H1 = a as Subset of U0 ;
consider H2 being Element of Sub U0 such that
H2 in H and
A5: H1 = (Carr U0) . H2 by A4, FUNCT_2:65;
A6: H1 = the carrier of H2 by A5, Def4;
then reconsider H3 = H1 as non empty Subset of U0 ;
S c= H1 by A1, A4, SETFAM_1:3;
then reconsider s1 = s as FinSequence of H3 by FINSEQ_2:24;
H3 is opers_closed by A6, UNIALG_2:def 7;
then H3 is_closed_on o ;
then o . s1 in H3 by A3;
hence o . s in a ; :: thesis: verum
end;
hence o . s in S by A1, A2, SETFAM_1:def 1; :: thesis: verum
end;
hence S is opers_closed ; :: thesis: verum