let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subalgebra of B ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
let A be non empty Subalgebra of B; :: thesis: ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
take C = the carrier of A; :: thesis: ( C is Subset of B & the carrier of A = C & C is opers_closed )
A1: ( 1. B = 1. A & 0. B = 0. A ) by Def3;
reconsider C = C as Subset of B by Def3;
A2: for a being Element of L
for v being Element of B st v in C holds
a * v in C

proof

let a be Element of L; :: thesis: for v being Element of B st v in C holds
a * v in C
let v be Element of B; :: thesis: ( v in C implies a * v in C )
assume v in C ; :: thesis: a * v in C
then reconsider x = v as Element of A ;
a * v = a * x by Th17;
hence a * v in C ; :: thesis: verum

end;

A3: for x, y being Element of B st x in C & y in C holds
x * y in C

proof

let x, y be Element of B; :: thesis: ( x in C & y in C implies x * y in C )
assume A4: ( x in C & y in C ) ; :: thesis: x * y in C
reconsider x9 = x, y9 = y as Element of B ;
reconsider x1 = x9, y1 = y9 as Element of A by A4;
x * y = x1 * y1 by Th16;
hence x * y in C ; :: thesis: verum

end;

for v, u being Element of B st v in C & u in C holds
v + u in C

proof

let v, u be Element of B; :: thesis: ( v in C & u in C implies v + u in C )
assume ( v in C & u in C ) ; :: thesis: v + u in C
then reconsider x = u, y = v as Element of A ;
v + u = y + x by Th15;
hence v + u in C ; :: thesis: verum

end;

then C is linearly-closed by A2, VECTSP_4:def 1;
hence ( C is Subset of B & the carrier of A = C & C is opers_closed ) by A1, A3, Def4; :: thesis: verum