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

proof

assume A1: X = bool Y ; :: thesis: for A being ManySortedSet of I holds
( A in X iff A c= Y )
let A be ManySortedSet of I; :: 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 object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or A . i c= Y . i )
assume A3: i in I ; :: thesis: A . i c= Y . i
then A4: A . i in X . i by A2;
X . i = bool (Y . i) by A1, A3, Def1;
hence A . i c= Y . i by A4; :: thesis: verum

end;

assume A5: A c= Y ; :: thesis: A in X
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in X . i )
assume A6: i in I ; :: thesis: A . i in X . i
then A7: A . i c= Y . i by A5;
X . i = bool (Y . i) by A1, A6, Def1;
hence A . i in X . i by A7; :: thesis: verum

end;

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

now :: thesis: for i being object st i in I holds
X . i = (bool Y) . i

let i be object ; :: thesis: ( i in I implies X . i = (bool Y) . i )
assume A9: i in I ; :: thesis: X . i = (bool Y) . i
EmptyMS I c= Y by PBOOLE:43;
then A10: EmptyMS I in X by A8;
for A9 being set holds
( A9 in X . i iff A9 c= Y . i )

proof

let A9 be set ; :: thesis: ( A9 in X . i iff A9 c= Y . i )
A11: dom (i .--> A9) = {i} ;
dom ((EmptyMS I) +* (i .--> A9)) = I by A9, Lm1;
then reconsider K = (EmptyMS I) +* (i .--> A9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A12: K . i = (i .--> A9) . i by A11, FUNCT_4:13
.= A9 by FUNCOP_1:72 ;
thus ( A9 in X . i implies A9 c= Y . i ) :: thesis: ( A9 c= Y . i implies A9 in X . i )

proof

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

proof

let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or K . j in X . j )
assume A14: j in I ; :: thesis: K . j in X . j

now :: thesis: ( ( j = i & K . j in X . j ) or ( j <> i & K . j in X . j ) )

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

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

hence K . j in X . j by A12, A13; :: thesis: verum

end;

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

then not j in dom (i .--> A9) by TARSKI:def 1;
then K . j = (EmptyMS I) . j by FUNCT_4:11;
hence K . j in X . j by A10, A14; :: thesis: verum

end;

end;

end;

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

end;

then K c= Y by A8;
hence A9 c= Y . i by A9, A12; :: thesis: verum

end;

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

proof

let j be object ; :: according to PBOOLE:def 2 :: thesis: ( not j in I or K . j c= Y . j )
assume A16: j in I ; :: thesis: K . j c= Y . j

now :: thesis: ( ( j = i & K . j c= Y . j ) or ( j <> i & K . j c= Y . j ) )

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

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

hence K . j c= Y . j by A12, A15; :: thesis: verum

end;

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

then not j in dom (i .--> A9) by TARSKI:def 1;
then A17: K . j = (EmptyMS I) . j by FUNCT_4:11;
EmptyMS I c= Y by PBOOLE:43;
hence K . j c= Y . j by A16, A17; :: thesis: verum

end;

end;

end;

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

end;

then K in X by A8;
hence A9 in X . i by A9, A12; :: thesis: verum

end;

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

end;

hence X = bool Y ; :: thesis: verum