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 is monotone

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 is monotone

let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: f -extension_to_hom is monotone

let F1, F2 be Element of (InclPoset (Filt (BoolePoset X))); :: according to ORDERS_3:def 5 :: thesis: ( not F1 <= F2 or for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (f -extension_to_hom) . F1 or not b_{2} = (f -extension_to_hom) . F2 or b_{1} <= b_{2} ) )

set F = f -extension_to_hom ;

set F1s = { ("/\" ( { (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 F1 } ;

set F2s = { ("/\" ( { (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 F2 } ;

A1: ( ex_sup_of { ("/\" ( { (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 F1 } ,L & ex_sup_of { ("/\" ( { (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 F2 } ,L ) by YELLOW_0:17;

A2: (f -extension_to_hom) . F1 = "\/" ( { ("/\" ( { (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 F1 } ,L) by Def3;

assume F1 <= F2 ; :: thesis: for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (f -extension_to_hom) . F1 or not b_{2} = (f -extension_to_hom) . F2 or b_{1} <= b_{2} )

then A3: F1 c= F2 by YELLOW_1:3;

A4: { ("/\" ( { (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 F1 } c= { ("/\" ( { (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 F2 }

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in F2 } ,L) by Def3;

let FF1, FF2 be Element of L; :: thesis: ( not FF1 = (f -extension_to_hom) . F1 or not FF2 = (f -extension_to_hom) . F2 or FF1 <= FF2 )

assume ( FF1 = (f -extension_to_hom) . F1 & FF2 = (f -extension_to_hom) . F2 ) ; :: thesis: FF1 <= FF2

hence FF1 <= FF2 by A2, A5, A1, A4, YELLOW_0:34; :: thesis: verum

for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone

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 is monotone

let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: f -extension_to_hom is monotone

let F1, F2 be Element of (InclPoset (Filt (BoolePoset X))); :: according to ORDERS_3:def 5 :: thesis: ( not F1 <= F2 or for b

( not b

set F = f -extension_to_hom ;

set F1s = { ("/\" ( { (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 F1 } ;

set F2s = { ("/\" ( { (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 F2 } ;

A1: ( ex_sup_of { ("/\" ( { (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 F1 } ,L & ex_sup_of { ("/\" ( { (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 F2 } ,L ) by YELLOW_0:17;

A2: (f -extension_to_hom) . F1 = "\/" ( { ("/\" ( { (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 F1 } ,L) by Def3;

assume F1 <= F2 ; :: thesis: for b

( not b

then A3: F1 c= F2 by YELLOW_1:3;

A4: { ("/\" ( { (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 F1 } c= { ("/\" ( { (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 F2 }

proof

A5:
(f -extension_to_hom) . F2 = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s 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 F1 } or s 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 F2 } )

assume s 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 F1 } ; :: thesis: s 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 F2 }

then ex Y being Subset of X st

( s = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) & Y in F1 ) ;

hence s 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 F2 } by A3; :: thesis: verum

end;( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in F1 } or s 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 F2 } )

assume s 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 F1 } ; :: thesis: s 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 F2 }

then ex Y being Subset of X st

( s = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) & Y in F1 ) ;

hence s 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 F2 } by A3; :: thesis: verum

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in F2 } ,L) by Def3;

let FF1, FF2 be Element of L; :: thesis: ( not FF1 = (f -extension_to_hom) . F1 or not FF2 = (f -extension_to_hom) . F2 or FF1 <= FF2 )

assume ( FF1 = (f -extension_to_hom) . F1 & FF2 = (f -extension_to_hom) . F2 ) ; :: thesis: FF1 <= FF2

hence FF1 <= FF2 by A2, A5, A1, A4, YELLOW_0:34; :: thesis: verum