let I be set ; :: thesis: for A, B being ManySortedSet of holds bool (A \ B) c= (I --> {{} }) \/ ((bool A) \ (bool B))
let A, B be ManySortedSet of ; :: thesis: bool (A \ B) c= (I --> {{} }) \/ ((bool A) \ (bool B))
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (bool (A \ B)) . i c= ((I --> {{} }) \/ ((bool A) \ (bool B))) . i )
assume A1: i in I ; :: thesis: (bool (A \ B)) . i c= ((I --> {{} }) \/ ((bool A) \ (bool B))) . i
then A2: (bool (A \ B)) . i = bool ((A . i) \ (B . i)) by Lm4;
((I --> {{} }) \/ ((bool A) \ (bool B))) . i = ((I --> {{} }) . i) \/ (((bool A) \ (bool B)) . i) by A1, PBOOLE:def 7
.= {{} } \/ (((bool A) \ (bool B)) . i) by A1, FUNCOP_1:13
.= {{} } \/ (((bool A) . i) \ ((bool B) . i)) by A1, PBOOLE:def 9
.= {{} } \/ ((bool (A . i)) \ ((bool B) . i)) by A1, Def1
.= {{} } \/ ((bool (A . i)) \ (bool (B . i))) by A1, Def1 ;
hence (bool (A \ B)) . i c= ((I --> {{} }) \/ ((bool A) \ (bool B))) . i by A2, ZFMISC_1:84; :: thesis: verum