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;

( 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

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

( 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

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 :: thesis: for p being object holds

( ( 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 } ) )

then A13:
{ ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( 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 } ) )

let p be object ; :: 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 } ) )

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

( 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

( 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

then A15:
"\/" ((union { { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
let r be object ; :: 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 )

reconsider rr = r as set by TARSKI:1;

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

rr c= the carrier of L

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

reconsider rr = r as set by TARSKI:1;

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

rr c= the carrier of L

proof

hence
r in bool the carrier of L
; :: thesis: verum
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in rr or s in the carrier of L )

assume s in rr ; :: 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;assume s in rr ; :: 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

( 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 :: thesis: for r being object holds

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

(f -extension_to_hom) . sFs = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( 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 ) )

let r be object ; :: 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 ) )

( 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:35; :: thesis: verum

end;( 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 { (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 object 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:64;

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

( 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;( 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 object 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:64;

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

then reconsider Zi = { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
let t be object ; :: 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;( 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

( 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

( 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:35; :: thesis: verum

( 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