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

proof

assume A2: for i being object st i in I holds
Y . i in X . i ; :: thesis: contradiction
consider i being object 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 (I,Y,X) ; :: thesis: verum