theorem :: MONOID_0:66

for A, B being non empty set st A c= B holds
A *+^ is SubStr of B *+^