set IP = InclPoset (Filt (BoolePoset X));
deffunc H₁( 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₁(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