let I be set ; for A, B being ManySortedSet of I st (bool A) (\/) (bool B) = bool (A (\/) B) holds
for i being set st i in I holds
A . i,B . i are_c=-comparable
let A, B be ManySortedSet of I; ( (bool A) (\/) (bool B) = bool (A (\/) B) implies for i being set st i in I holds
A . i,B . i are_c=-comparable )
assume A1:
(bool A) (\/) (bool B) = bool (A (\/) B)
; for i being set st i in I holds
A . i,B . i are_c=-comparable
let i be set ; ( i in I implies A . i,B . i are_c=-comparable )
assume A2:
i in I
; A . i,B . i are_c=-comparable
bool ((A . i) \/ (B . i)) =
((bool A) (\/) (bool B)) . i
by A1, A2, Lm2
.=
((bool A) . i) \/ ((bool B) . i)
by A2, PBOOLE:def 4
.=
((bool A) . i) \/ (bool (B . i))
by A2, Def1
.=
(bool (A . i)) \/ (bool (B . i))
by A2, Def1
;
hence
A . i,B . i are_c=-comparable
by ZFMISC_1:70; verum