let I be set ; :: thesis: for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X (\/) Y))
let X, Y be ManySortedSet of I; :: thesis: [|X,Y|] c= bool (bool (X (\/) Y))
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or [|X,Y|] . i c= (bool (bool (X (\/) Y))) . i )
assume A1: i in I ; :: thesis: [|X,Y|] . i c= (bool (bool (X (\/) Y))) . i
then A2: [|X,Y|] . i = [:(X . i),(Y . i):] by PBOOLE:def 16;
(bool (bool (X (\/) Y))) . i = bool ((bool (X (\/) Y)) . i) by A1, Def1
.= bool (bool ((X . i) \/ (Y . i))) by A1, Lm2 ;
hence [|X,Y|] . i c= (bool (bool (X (\/) Y))) . i by A2, ZFMISC_1:86; :: thesis: verum