theorem :: WAYBEL22:12

for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone