theorem Th3: :: LTLAXIO3:3

for D1, D2 being set st D1 c= D2 holds
D1 ** c= D2 **