let L be non empty multMagma ; :: thesis:
let B be non empty AlgebraStr over L; :: thesis:
let A be non empty Subset of B; :: thesis:
let X be Subset-Family of B; :: thesis:
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

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

reconsider x9 = x, y9 = y as Element of B ;
let Y be set ; :: thesis:
assume A5: Y in X ; :: thesis:
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:

end;

end;

for a being Element of L
for v being Element of B st v in meet X holds
a * v in meet X

let Y be set ; :: thesis:
assume A9: Y in X ; :: thesis:
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:

end;

end;

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

reconsider x9 = x, y9 = y as Element of B ;
let Y be set ; :: thesis:
assume A13: Y in X ; :: thesis:
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:

end;

end;

let Y be set ; :: thesis:
assume Y in X ; :: thesis:
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:

end;

let Y be set ; :: thesis:
assume Y in X ; :: thesis:
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:

end;