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

x * y in C

v + u in C

hence ( C is Subset of B & the carrier of A = C & C is opers_closed ) by A1, A3, Def4; :: thesis: verum

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

A3:
for x, y being Element of B st x in C & y in C holds
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;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

x * y in C

proof

for v, u being Element of B st v in C & u in C holds
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;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

v + u in C

proof

then
C is linearly-closed
by A2, VECTSP_4:def 1;
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;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

hence ( C is Subset of B & the carrier of A = C & C is opers_closed ) by A1, A3, Def4; :: thesis: verum