theorem Th15: :: WAYBEL22:15

for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom