let L be non empty multMagma ; :: thesis:
let B be non empty AlgebraStr of 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;
thus meet X is linearly-closed :: according to POLYALG1:def 4 :: thesis:

proof

thus for x, y being Element of B st x in meet X & y in meet X holds
x + y in meet X :: according to VECTSP_4:def 1 :: thesis:

proof

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

now

let Y be set ; :: thesis:
assume A4: Y in X ; :: thesis:
then consider C being Subalgebra of B such that
A5: ( Y = the carrier of C & A c= Y ) by A1;
consider a being set ;
reconsider C = C as non empty Subalgebra of B by A5;
reconsider x' = x, y' = y as Element of B ;
reconsider x1 = x', y1 = y' as Element of C by A3, A4, A5, SETFAM_1:def 1;
x + y = x1 + y1 by Th15;
hence x + y in Y by A5; :: thesis:

end;

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

end;

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

proof

let a be Element of L; :: thesis:
let v be Element of B; :: thesis:
assume A7: v in meet X ; :: thesis:

now

let Y be set ; :: thesis:
assume A8: Y in X ; :: thesis:
then consider C being Subalgebra of B such that
A9: ( Y = the carrier of C & A c= Y ) by A1;
consider z being set ;
reconsider C = C as non empty Subalgebra of B by A9;
reconsider v' = v as Element of C by A7, A8, A9, SETFAM_1:def 1;
a * v = a * v' by Th17;
hence a * v in Y by A9; :: thesis:

end;

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

end;

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

proof

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

now

let Y be set ; :: thesis:
assume A12: Y in X ; :: thesis:
then consider C being Subalgebra of B such that
A13: ( Y = the carrier of C & A c= Y ) by A1;
consider a being set ;
reconsider C = C as non empty Subalgebra of B by A13;
reconsider x' = x, y' = y as Element of B ;
reconsider x1 = x', y1 = y' as Element of C by A11, A12, A13, SETFAM_1:def 1;
x * y = x1 * y1 by Th16;
hence x * y in Y by A13; :: thesis:

end;

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

end;

now

let Y be set ; :: thesis:
assume Y in X ; :: thesis:
then consider C being Subalgebra of B such that
A15: ( Y = the carrier of C & A c= Y ) by A1;
consider a being set ;
reconsider C = C as non empty Subalgebra of B by A15;
1. B = 1. C by Def3;
hence 1. B in Y by A15; :: thesis:

end;

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

now

let Y be set ; :: thesis:
assume Y in X ; :: thesis:
then consider C being Subalgebra of B such that
A17: ( Y = the carrier of C & A c= Y ) by A1;
consider a being set ;
reconsider C = C as non empty Subalgebra of B by A17;
0. B = 0. C by Def3;
hence 0. B in Y by A17; :: thesis:

end;

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