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 ) } = {}

( 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;

hence (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A3, WAYBEL15:3; :: thesis: verum

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

A3:
(f -extension_to_hom) . T = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
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 object 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;( x = {z} & z in E ) } = {} ; :: thesis: contradiction

then consider r being object 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

( 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;

hence (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A3, WAYBEL15:3; :: thesis: verum