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