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:
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
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
now :: thesis: for Y being set st Y in X holds
x + 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 ;
x + y = x1 + y1 by Th15;
hence x + y in Y by A6; :: thesis: verum
end;
hence x + y in meet X by ; :: thesis: verum
end;
for a being Element of L
for v being Element of B st v in meet X holds
a * v in meet X
proof
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
now :: thesis: for Y being set st Y in X holds
a * 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 ;
reconsider v9 = v as Element of C by ;
a * v = a * v9 by Th17;
hence a * v in Y by A10; :: thesis: verum
end;
hence a * v in meet X by ; :: thesis: verum
end;
hence meet X is linearly-closed by ; :: according to POLYALG1:def 4 :: thesis: ( ( for x, y being Element of B st x in meet X & y in meet X holds
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
now :: thesis: for Y being set st Y in X holds
x * 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 ;
reconsider x1 = x9, y1 = y9 as Element of C by ;
x * y = x1 * y1 by Th16;
hence x * y in Y by A14; :: thesis: verum
end;
hence x * y in meet X by ; :: thesis: verum
end;
now :: thesis: for Y being set st Y in X holds
1. 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 ;
1. B = 1. C by Def3;
hence 1. B in Y by A16; :: thesis: verum
end;
hence 1. B in meet X by ; :: thesis: 0. B in meet X
now :: thesis: for Y being set st Y in X holds
0. 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 ;
0. B = 0. C by Def3;
hence 0. B in Y by A18; :: thesis: verum
end;
hence 0. B in meet X by ; :: thesis: verum