theorem Th14:
for
L being
1-sorted for
A,
B being
AlgebraStr over
L st
AlgebraStr(# the
carrier of
A, the
addF of
A, the
multF of
A, the
ZeroF of
A, the
OneF of
A, the
lmult of
A #)
= AlgebraStr(# the
carrier of
B, the
addF of
B, the
multF of
B, the
ZeroF of
B, the
OneF of
B, the
lmult of
B #) holds
A is
Subalgebra of
B