let I be set ; for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X (\/) Y))
let X, Y be ManySortedSet of I; [|X,Y|] c= bool (bool (X (\/) Y))
let i be object ; PBOOLE:def 2 ( not i in I or [|X,Y|] . i c= (bool (bool (X (\/) Y))) . i )
assume A1:
i in I
; [|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; verum