let L be non empty multMagma ; 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; 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; ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
take C = the carrier of A; ( 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
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;
( x in C & y in C implies x * y in C )
assume A4:
(
x in C &
y in C )
;
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
;
verum
end;
for v, u being Element of B st v in C & u in C holds
v + u in C
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; verum