set IP = InclPoset (Filt (BoolePoset X));
let it1, it2 be Function of (InclPoset (Filt (BoolePoset X))),L; ( ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . 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) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . 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) ) implies it1 = it2 )
assume that
A2:
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . 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)
and
A3:
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . 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)
; it1 = it2
reconsider it29 = it2 as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
reconsider it19 = it1 as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
hence
it1 = it2
by FUNCT_2:63; verum