set IP = InclPoset (Filt (BoolePoset X));
let it1, it2 be Function of (InclPoset (Filt (BoolePoset X))),L; :: thesis: ( ( 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) ; :: thesis: 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 ;
now :: thesis: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it19 . Fi = it29 . Fi
let Fi be Element of (InclPoset (Filt (BoolePoset X))); :: thesis: it19 . Fi = it29 . Fi
thus it19 . 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 A2
.= it29 . Fi by A3 ; :: thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; :: thesis: verum