Что-то не получается доказать такой факт, с которым я столкнулся в теории верификации программ.
Есть

-- функция, отображающая множество

всех подмножеств

в себя. При этом она монотонна (если

то

). Определим на

отношение частичного порядка как теоретико-множественное включение. Нужно доказать, что минимальная неподвижная точка отображения

определяется как

Подскажите, как это сделать?