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 h' being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h' | (FixedUltraFilters X) = f holds
h' = 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 h' being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h' | (FixedUltraFilters X) = f holds
h' = 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 h' being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h' | (FixedUltraFilters X) = f holds
h' = F ) )
thus F | (FixedUltraFilters X) = f by Th14; :: thesis: for h' being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h' | (FixedUltraFilters X) = f holds
h' = F
let h' be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; :: thesis: ( h' | (FixedUltraFilters X) = f implies h' = F )
assume h' | (FixedUltraFilters X) = f ; :: thesis: h' = F
hence h' = F by Th15; :: thesis: verum