let X, Y be ManySortedSet of I; :: thesis: ( X in Y implies not Y in X )
assume A1: for i being set st i in I holds
X . i in Y . i ; :: according to PBOOLE:def 1 :: thesis: not Y in X
ex i being set st
( i in I & not Y . i in X . i )

proof

assume A2: for i being set st i in I holds
Y . i in X . i ; :: thesis: contradiction
consider i being set such that
A3: i in I by XBOOLE_0:def 1;
X . i in Y . i by A1, A3;
hence contradiction by A2, A3; :: thesis: verum

end;

hence not Y in X by Def4; :: thesis: verum