theorem Th9: :: CIRCLED1:9

for V being RealLinearSpace
for M1, M2 being Subset of V st M1 c= M2 holds
Circled-Family M2 c= Circled-Family M1