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₁, b₂ being Element of the carrier of L holds
( not b₁ = (f -extension_to_hom ) . F1 or not b₂ = (f -extension_to_hom ) . F2 or b₁ <= b₂ ) )
assume F1 <= F2 ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (f -extension_to_hom ) . F1 or not b₂ = (f -extension_to_hom ) . F2 or b₁ <= b₂ )
then A1: F1 c= F2 by YELLOW_1:3;
set F = f -extension_to_hom ;
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 A2: ( FF1 = (f -extension_to_hom ) . F1 & FF2 = (f -extension_to_hom ) . F2 ) ; :: thesis: FF1 <= FF2
A3: (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;
A4: (f -extension_to_hom ) . F2 = "\/" { ("/\" { (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 Def3;
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 } ;
A5: 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 by YELLOW_0:17;
A6: 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;
{ ("/\" { (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

let s be set ; :: 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 consider Y being Subset of X such that
A7: s = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L and
A8: Y in F1 ;
thus 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 A1, A7, A8; :: thesis: verum

end;

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