set IP = InclPoset (Filt (BoolePoset X));

deffunc H_{1}( Element of (InclPoset (Filt (BoolePoset X)))) -> Element of the carrier of 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 $1 } ,L);

consider F being Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L such that

A1: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = H_{1}(Fi)
from FUNCT_2:sch 4();

reconsider F = F as Function of (InclPoset (Filt (BoolePoset X))),L ;

take F ; :: thesis: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L)

thus for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) by A1; :: thesis: verum

deffunc H

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in $1 } ,L);

consider F being Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L such that

A1: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = H

reconsider F = F as Function of (InclPoset (Filt (BoolePoset X))),L ;

take F ; :: thesis: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L)

thus for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) by A1; :: thesis: verum