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

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

hence
S is opers_closed
; :: thesis: verum
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

end;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

hence
o . s in S
by A1, A2, SETFAM_1:def 1; :: thesis: verumo . 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;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