let I be set ; :: thesis: for X, Y being ManySortedSet of holds
( X = bool Y iff for A being ManySortedSet of holds
( A in X iff A c= Y ) )
let X, Y be ManySortedSet of ; :: thesis: ( X = bool Y iff for A being ManySortedSet of holds
( A in X iff A c= Y ) )
thus ( X = bool Y implies for A being ManySortedSet of holds
( A in X iff A c= Y ) ) :: thesis: ( ( for A being ManySortedSet of holds
( A in X iff A c= Y ) ) implies X = bool Y )

proof

assume A1: X = bool Y ; :: thesis: for A being ManySortedSet of holds
( A in X iff A c= Y )
let A be ManySortedSet of ; :: thesis: ( A in X iff A c= Y )
thus ( A in X implies A c= Y ) :: thesis: ( A c= Y implies A in X )

proof

assume A2: A in X ; :: thesis: A c= Y
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or A . i c= Y . i )
assume i in I ; :: thesis: A . i c= Y . i
then ( X . i = bool (Y . i) & A . i in X . i ) by A1, A2, Def1, PBOOLE:def 4;
hence A . i c= Y . i ; :: thesis: verum

end;

assume A3: A c= Y ; :: thesis: A in X
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or A . i in X . i )
assume i in I ; :: thesis: A . i in X . i
then ( X . i = bool (Y . i) & A . i c= Y . i ) by A1, A3, Def1, PBOOLE:def 5;
hence A . i in X . i ; :: thesis: verum

end;

assume A4: for A being ManySortedSet of holds
( A in X iff A c= Y ) ; :: thesis: X = bool Y

now

let i be set ; :: thesis: ( i in I implies X . i = (bool Y) . i )
assume A5: i in I ; :: thesis: X . i = (bool Y) . i
[0] I c= Y by PBOOLE:49;
then A6: [0] I in X by A4;
for A' being set holds
( A' in X . i iff A' c= Y . i )

proof

let A' be set ; :: thesis: ( A' in X . i iff A' c= Y . i )
A7: dom (i .--> A') = {i} by FUNCOP_1:19;
dom (([0] I) +* (i .--> A')) = I by A5, Lm1;
then reconsider K = ([0] I) +* (i .--> A') as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A8: K . i = (i .--> A') . i by A7, FUNCT_4:14
.= A' by FUNCOP_1:87 ;
thus ( A' in X . i implies A' c= Y . i ) :: thesis: ( A' c= Y . i implies A' in X . i )

proof

assume A9: A' in X . i ; :: thesis: A' c= Y . i
K in X

proof

let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or K . j in X . j )
assume A10: j in I ; :: thesis: K . j in X . j

now

per cases ( j = i or j <> i ) ;

case j = i ; :: thesis: K . j in X . j

hence K . j in X . j by A8, A9; :: thesis: verum

end;

case j <> i ; :: thesis: K . j in X . j

then not j in dom (i .--> A') by A7, TARSKI:def 1;
then K . j = ([0] I) . j by FUNCT_4:12;
hence K . j in X . j by A6, A10, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

hence K . j in X . j ; :: thesis: verum

end;

then K c= Y by A4;
hence A' c= Y . i by A5, A8, PBOOLE:def 5; :: thesis: verum

end;

assume A11: A' c= Y . i ; :: thesis: A' in X . i
K c= Y

proof

let j be set ; :: according to PBOOLE:def 5 :: thesis: ( not j in I or K . j c= Y . j )
assume A12: j in I ; :: thesis: K . j c= Y . j

now

per cases ( j = i or j <> i ) ;

case j = i ; :: thesis: K . j c= Y . j

hence K . j c= Y . j by A8, A11; :: thesis: verum

end;

case j <> i ; :: thesis: K . j c= Y . j

then not j in dom (i .--> A') by A7, TARSKI:def 1;
then A13: K . j = ([0] I) . j by FUNCT_4:12;
[0] I c= Y by PBOOLE:49;
hence K . j c= Y . j by A12, A13, PBOOLE:def 5; :: thesis: verum

end;

end;

end;

hence K . j c= Y . j ; :: thesis: verum

end;

then K in X by A4;
hence A' in X . i by A5, A8, PBOOLE:def 4; :: thesis: verum

end;

then X . i = bool (Y . i) by ZFMISC_1:def 1;
hence X . i = (bool Y) . i by A5, Def1; :: thesis: verum

end;

hence X = bool Y by PBOOLE:3; :: thesis: verum