let I be set ; :: thesis: 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; :: thesis: ( (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) ; :: thesis: for i being set st i in I holds
A . i,B . i are_c=-comparable
let i be set ; :: thesis: ( i in I implies A . i,B . i are_c=-comparable )
assume A2: i in I ; :: thesis: 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; :: thesis: verum