let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr of 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 of 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 )
reconsider C = C as Subset of B by Def3;
A1: C is linearly-closed

proof

thus for v, u being Element of B st v in C & u in C holds
v + u in C :: according to VECTSP_4:def 1 :: thesis: for b₁ being Element of the carrier of L
for b₂ being Element of the carrier of B holds
( not b₂ in C or b₁ * b₂ in C )

proof

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

end;

thus for a being Element of L
for v being Element of B st v in C holds
a * v in C :: thesis: verum

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 A3: v in C ; :: thesis: a * v in C
reconsider x = v as Element of A by A3;
a * v = a * x by Th17;
hence a * v in C ; :: thesis: verum

end;

end;

A4: ( 1. B = 1. A & 0. B = 0. A ) by Def3;
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 A5: ( x in C & y in C ) ; :: thesis: x * y in C
reconsider x' = x, y' = y as Element of B ;
reconsider x1 = x', y1 = y' as Element of A by A5;
x * y = x1 * y1 by Th16;
hence x * y in C ; :: thesis: verum

end;

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