let I be set ; :: thesis: for A being ManySortedSet of I holds A c= bool (union A)
let A be ManySortedSet of I; :: thesis: A c= bool (union A)
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or A . i c= (bool (union A)) . i )
assume A1: i in I ; :: thesis: A . i c= (bool (union A)) . i
then (bool (union A)) . i = bool ((union A) . i) by Def1
.= bool (union (A . i)) by A1, Def2 ;
hence A . i c= (bool (union A)) . i by ZFMISC_1:82; :: thesis: verum