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))) ;
A1: (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;
A2: T = bool X by WAYBEL16:15;
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 } ;
A3: "/\" { (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 } by A2;
A4: { (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
A5: 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;
consider x being Element of (BoolePoset X) such that
r = f . (uparrow x) and
A6: ex z being Element of X st
( x = {z} & z in E ) by A5;
thus contradiction by A6; :: thesis: verum

end;

{ ("/\" { (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 A3, A4, LATTICE3:def 9;
hence (f -extension_to_hom ) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A1, WAYBEL15:5; :: thesis: verum