let I be set ; :: thesis: for A, B being ManySortedSet of I holds (bool A) (\/) (bool B) c= bool (A (\/) B)
let A, B be ManySortedSet of I; :: thesis: (bool A) (\/) (bool B) c= bool (A (\/) B)
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or ((bool A) (\/) (bool B)) . i c= (bool (A (\/) B)) . i )
assume A1: i in I ; :: thesis: ((bool A) (\/) (bool B)) . i c= (bool (A (\/) B)) . i
then A2: (bool (A (\/) B)) . i = bool ((A . i) \/ (B . i)) by Lm2;
((bool A) (\/) (bool B)) . i = ((bool A) . i) \/ ((bool B) . i) by A1, PBOOLE:def 4
.= (bool (A . i)) \/ ((bool B) . i) by A1, Def1
.= (bool (A . i)) \/ (bool (B . i)) by A1, Def1 ;
hence ((bool A) (\/) (bool B)) . i c= (bool (A (\/) B)) . i by A2, ZFMISC_1:69; :: thesis: verum