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:
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 ;
A6: H1 = the carrier of H2 by ;
then reconsider H3 = H1 as non empty Subset of U0 ;
S c= H1 by ;
then reconsider s1 = s as FinSequence of H3 by FINSEQ_2:24;
H3 is opers_closed by ;
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 ; :: thesis: verum
end;
hence S is opers_closed ; :: thesis: verum