let X be set ; :: thesis: FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))
set FUF = FixedUltraFilters X;
set IP = InclPoset (Filt (BoolePoset X));
let L be non empty complete continuous Poset; :: according to WAYBEL22:def 1 :: thesis: for f being Function of (FixedUltraFilters X), the carrier of L ex h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st
( h | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = h ) )
let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: ex h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st
( h | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = h ) )
reconsider F = f -extension_to_hom as CLHomomorphism of InclPoset (Filt (BoolePoset X)),L by WAYBEL16:def 1;
take F ; :: thesis: ( F | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = F ) )
thus F | (FixedUltraFilters X) = f by Th14; :: thesis: for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = F
let h9 be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; :: thesis: ( h9 | (FixedUltraFilters X) = f implies h9 = F )
assume h9 | (FixedUltraFilters X) = f ; :: thesis: h9 = F
hence h9 = F by Th15; :: thesis: verum