theorem :: KURATO_0:22

for T being set
for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T