set F = f -extension_to_hom ;
set IP = InclPoset (Filt (BoolePoset X));
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def 37 :: thesis: ( Fs is empty or not Fs is directed or f -extension_to_hom preserves_sup_of Fs )
assume A1: ( not Fs is empty & Fs is directed ) ; :: thesis: f -extension_to_hom preserves_sup_of Fs
reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A1;
set FFsU = { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } ;
reconsider sFs = sup Fs as Element of (InclPoset (Filt (BoolePoset X))) ;
set FFs = { ("/\" { (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 sFs } ;
A2: sup Fs = union Fs by A1, Th1;

now

let p be set ; :: thesis: ( ( p 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 sFs } implies p in union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } ) & ( p in union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } implies p 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 sFs } ) )

hereby :: thesis: ( p in union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } implies p 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 sFs } )

assume p 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 sFs } ; :: thesis: p in union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum }
then consider Y being Subset of X such that
A3: p = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L and
A4: Y in sFs ;
consider YY being set such that
A5: Y in YY and
A6: YY in Fs by A2, A4, TARSKI:def 4;
A7: { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y1 ) } ,L) where Y1 is Subset of X : Y1 in YY } 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 YY } where YY is Element of Fs9 : verum } by A6;
p in { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y1 ) } ,L) where Y1 is Subset of X : Y1 in YY } by A3, A5;
hence p in union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } by A7, TARSKI:def 4; :: thesis: verum

end;

assume p in union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } ; :: thesis: p 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 sFs }
then consider r being set such that
A8: p in r and
A9: r 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 YY } where YY is Element of Fs9 : verum } by TARSKI:def 4;
consider YY being Element of Fs9 such that
A10: r = { ("/\" { (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 YY } by A9;
consider Y being Subset of X such that
A11: p = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L and
A12: Y in YY by A8, A10;
Y in sFs by A2, A12, TARSKI:def 4;
hence p 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 sFs } by A11; :: thesis: verum

end;

then A13: { ("/\" { (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 sFs } = union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } by TARSKI:2;
set Zs = { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ;
assume ex_sup_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (f -extension_to_hom ) .: Fs,L & "\/" ((f -extension_to_hom ) .: Fs),L = (f -extension_to_hom ) . ("\/" Fs,(InclPoset (Filt (BoolePoset X)))) )
thus ex_sup_of (f -extension_to_hom ) .: Fs,L by YELLOW_0:17; :: thesis: "\/" ((f -extension_to_hom ) .: Fs),L = (f -extension_to_hom ) . ("\/" Fs,(InclPoset (Filt (BoolePoset X))))
{ { ("/\" { (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 YY } where YY is Element of Fs9 : verum } c= bool the carrier of L

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r 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 YY } where YY is Element of Fs9 : verum } or r in bool the carrier of L )
assume r 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 YY } where YY is Element of Fs9 : verum } ; :: thesis: r in bool the carrier of L
then consider YY being Element of Fs9 such that
A14: r = { ("/\" { (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 YY } ;
r c= the carrier of L

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in r or s in the carrier of L )
assume s in r ; :: thesis: s in the carrier of L
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 YY ) by A14;
hence s in the carrier of L ; :: thesis: verum

end;

hence r in bool the carrier of L ; :: thesis: verum

end;

then A15: "\/" (union { { ("/\" { (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 YY } where YY is Element of Fs9 : verum } ),L = "\/" { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ,L by Lm2;

A16: now

let r be set ; :: thesis: ( ( r in (f -extension_to_hom ) .: Fs implies r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ) & ( r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } implies r in (f -extension_to_hom ) .: Fs ) )

hereby :: thesis: ( r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } implies r in (f -extension_to_hom ) .: Fs )

assume r in (f -extension_to_hom ) .: Fs ; :: thesis: r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } }
then consider YY being set such that
A17: YY in the carrier of (InclPoset (Filt (BoolePoset X))) and
A18: YY in Fs and
A19: (f -extension_to_hom ) . YY = r by FUNCT_2:115;
reconsider YY = YY as Element of Fs by A18;
reconsider YY9 = YY as Element of (InclPoset (Filt (BoolePoset X))) by A17;
set Zi = { ("/\" { (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 YY9 } ;
{ ("/\" { (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 YY9 } c= the carrier of L

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t 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 YY9 } or t in the carrier of L )
assume t 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 YY9 } ; :: thesis: t in the carrier of L
then ex Y being Subset of X st
( t = "/\" { (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 YY9 ) ;
hence t in the carrier of L ; :: thesis: verum

end;

then reconsider Zi = { ("/\" { (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 YY9 } as Subset of L ;
A20: Zi 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 YY } where YY is Element of Fs9 : verum } ;
(f -extension_to_hom ) . YY9 = "\/" { ("/\" { (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 YY9 } ,L by Def3;
hence r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } by A19, A20; :: thesis: verum

end;

assume r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ; :: thesis: r in (f -extension_to_hom ) .: Fs
then consider Z being Subset of L such that
A21: r = sup Z and
A22: Z 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 YY } where YY is Element of Fs9 : verum } ;
consider YY being Element of Fs such that
A23: 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 YY } by A22;
reconsider YY = YY as Element of Fs9 ;
reconsider YY9 = YY as Element of (InclPoset (Filt (BoolePoset X))) ;
(f -extension_to_hom ) . YY9 = "\/" { ("/\" { (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 YY9 } ,L by Def3;
hence r in (f -extension_to_hom ) .: Fs by A21, A23, FUNCT_2:43; :: thesis: verum

end;

(f -extension_to_hom ) . sFs = "\/" { ("/\" { (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 sFs } ,L by Def3;
hence "\/" ((f -extension_to_hom ) .: Fs),L = (f -extension_to_hom ) . ("\/" Fs,(InclPoset (Filt (BoolePoset X)))) by A15, A13, A16, TARSKI:2; :: thesis: verum