let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr over L

for A being non empty Subset of B

for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subset of B

for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

let A be non empty Subset of B; :: thesis: for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

let X be Subset-Family of B; :: thesis: ( ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) implies meet X is opers_closed )

assume A1: for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ; :: thesis: meet X is opers_closed

B is Subalgebra of B by Th11;

then A2: X <> {} by A1;

A3: for x, y being Element of B st x in meet X & y in meet X holds

x + y in meet X

for v being Element of B st v in meet X holds

a * v in meet X

x * y in meet X ) & 1. B in meet X & 0. B in meet X )

thus for x, y being Element of B st x in meet X & y in meet X holds

x * y in meet X :: thesis: ( 1. B in meet X & 0. B in meet X )

for A being non empty Subset of B

for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subset of B

for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

let A be non empty Subset of B; :: thesis: for X being Subset-Family of B st ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) holds

meet X is opers_closed

let X be Subset-Family of B; :: thesis: ( ( for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ) implies meet X is opers_closed )

assume A1: for Y being set holds

( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st

( Y = the carrier of C & A c= Y ) ) ) ; :: thesis: meet X is opers_closed

B is Subalgebra of B by Th11;

then A2: X <> {} by A1;

A3: for x, y being Element of B st x in meet X & y in meet X holds

x + y in meet X

proof

for a being Element of L
let x, y be Element of B; :: thesis: ( x in meet X & y in meet X implies x + y in meet X )

assume A4: ( x in meet X & y in meet X ) ; :: thesis: x + y in meet X

end;assume A4: ( x in meet X & y in meet X ) ; :: thesis: x + y in meet X

now :: thesis: for Y being set st Y in X holds

x + y in Y

hence
x + y in meet X
by A2, SETFAM_1:def 1; :: thesis: verumx + y in Y

reconsider x9 = x, y9 = y as Element of B ;

let Y be set ; :: thesis: ( Y in X implies x + y in Y )

assume A5: Y in X ; :: thesis: x + y in Y

then consider C being Subalgebra of B such that

A6: Y = the carrier of C and

A7: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A6, A7;

reconsider x1 = x9, y1 = y9 as Element of C by A4, A5, A6, SETFAM_1:def 1;

x + y = x1 + y1 by Th15;

hence x + y in Y by A6; :: thesis: verum

end;let Y be set ; :: thesis: ( Y in X implies x + y in Y )

assume A5: Y in X ; :: thesis: x + y in Y

then consider C being Subalgebra of B such that

A6: Y = the carrier of C and

A7: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A6, A7;

reconsider x1 = x9, y1 = y9 as Element of C by A4, A5, A6, SETFAM_1:def 1;

x + y = x1 + y1 by Th15;

hence x + y in Y by A6; :: thesis: verum

for v being Element of B st v in meet X holds

a * v in meet X

proof

hence
meet X is linearly-closed
by A3, VECTSP_4:def 1; :: according to POLYALG1:def 4 :: thesis: ( ( for x, y being Element of B st x in meet X & y in meet X holds
let a be Element of L; :: thesis: for v being Element of B st v in meet X holds

a * v in meet X

let v be Element of B; :: thesis: ( v in meet X implies a * v in meet X )

assume A8: v in meet X ; :: thesis: a * v in meet X

end;a * v in meet X

let v be Element of B; :: thesis: ( v in meet X implies a * v in meet X )

assume A8: v in meet X ; :: thesis: a * v in meet X

now :: thesis: for Y being set st Y in X holds

a * v in Y

hence
a * v in meet X
by A2, SETFAM_1:def 1; :: thesis: veruma * v in Y

let Y be set ; :: thesis: ( Y in X implies a * v in Y )

assume A9: Y in X ; :: thesis: a * v in Y

then consider C being Subalgebra of B such that

A10: Y = the carrier of C and

A11: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A10, A11;

reconsider v9 = v as Element of C by A8, A9, A10, SETFAM_1:def 1;

a * v = a * v9 by Th17;

hence a * v in Y by A10; :: thesis: verum

end;assume A9: Y in X ; :: thesis: a * v in Y

then consider C being Subalgebra of B such that

A10: Y = the carrier of C and

A11: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A10, A11;

reconsider v9 = v as Element of C by A8, A9, A10, SETFAM_1:def 1;

a * v = a * v9 by Th17;

hence a * v in Y by A10; :: thesis: verum

x * y in meet X ) & 1. B in meet X & 0. B in meet X )

thus for x, y being Element of B st x in meet X & y in meet X holds

x * y in meet X :: thesis: ( 1. B in meet X & 0. B in meet X )

proof

let x, y be Element of B; :: thesis: ( x in meet X & y in meet X implies x * y in meet X )

assume A12: ( x in meet X & y in meet X ) ; :: thesis: x * y in meet X

end;assume A12: ( x in meet X & y in meet X ) ; :: thesis: x * y in meet X

now :: thesis: for Y being set st Y in X holds

x * y in Y

hence
x * y in meet X
by A2, SETFAM_1:def 1; :: thesis: verumx * y in Y

reconsider x9 = x, y9 = y as Element of B ;

let Y be set ; :: thesis: ( Y in X implies x * y in Y )

assume A13: Y in X ; :: thesis: x * y in Y

then consider C being Subalgebra of B such that

A14: Y = the carrier of C and

A15: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A14, A15;

reconsider x1 = x9, y1 = y9 as Element of C by A12, A13, A14, SETFAM_1:def 1;

x * y = x1 * y1 by Th16;

hence x * y in Y by A14; :: thesis: verum

end;let Y be set ; :: thesis: ( Y in X implies x * y in Y )

assume A13: Y in X ; :: thesis: x * y in Y

then consider C being Subalgebra of B such that

A14: Y = the carrier of C and

A15: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A14, A15;

reconsider x1 = x9, y1 = y9 as Element of C by A12, A13, A14, SETFAM_1:def 1;

x * y = x1 * y1 by Th16;

hence x * y in Y by A14; :: thesis: verum

now :: thesis: for Y being set st Y in X holds

1. B in Y

hence
1. B in meet X
by A2, SETFAM_1:def 1; :: thesis: 0. B in meet X1. B in Y

let Y be set ; :: thesis: ( Y in X implies 1. B in Y )

assume Y in X ; :: thesis: 1. B in Y

then consider C being Subalgebra of B such that

A16: Y = the carrier of C and

A17: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A16, A17;

1. B = 1. C by Def3;

hence 1. B in Y by A16; :: thesis: verum

end;assume Y in X ; :: thesis: 1. B in Y

then consider C being Subalgebra of B such that

A16: Y = the carrier of C and

A17: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A16, A17;

1. B = 1. C by Def3;

hence 1. B in Y by A16; :: thesis: verum

now :: thesis: for Y being set st Y in X holds

0. B in Y

hence
0. B in meet X
by A2, SETFAM_1:def 1; :: thesis: verum0. B in Y

let Y be set ; :: thesis: ( Y in X implies 0. B in Y )

assume Y in X ; :: thesis: 0. B in Y

then consider C being Subalgebra of B such that

A18: Y = the carrier of C and

A19: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A18, A19;

0. B = 0. C by Def3;

hence 0. B in Y by A18; :: thesis: verum

end;assume Y in X ; :: thesis: 0. B in Y

then consider C being Subalgebra of B such that

A18: Y = the carrier of C and

A19: A c= Y by A1;

reconsider C = C as non empty Subalgebra of B by A18, A19;

0. B = 0. C by Def3;

hence 0. B in Y by A18; :: thesis: verum