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

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