let X be set ; :: thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X),the carrier of L holds (f -extension_to_hom ) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
let L be non empty complete continuous Poset; :: thesis: for f being Function of (FixedUltraFilters X),the carrier of L holds (f -extension_to_hom ) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
let f be Function of (FixedUltraFilters X),the carrier of L; :: thesis: (f -extension_to_hom ) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
set IP = InclPoset (Filt (BoolePoset X));
set F = f -extension_to_hom ;
reconsider T = Top (InclPoset (Filt (BoolePoset X))) as Element of (InclPoset (Filt (BoolePoset X))) ;
reconsider E = {} as Subset of X by XBOOLE_1:2;
set Z = { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in T } ;
A1: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } = {}

proof

assume not { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } = {} ; :: thesis: contradiction
then consider r being set such that
A2: r in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } by XBOOLE_0:def 1;
ex x being Element of (BoolePoset X) st
( r = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in E ) ) by A2;
hence contradiction ; :: thesis: verum

end;

A3: (f -extension_to_hom ) . T = "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in T } ,L by Def3;
T = bool X by WAYBEL16:15;
then A4: "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } ,L in { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in T } ;
{ ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in T } is_<=_than "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in T } ,L by YELLOW_0:32;
then Top L <= "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in T } ,L by A4, A1, LATTICE3:def 9;
hence (f -extension_to_hom ) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A3, WAYBEL15:5; :: thesis: verum