let I be set ; :: thesis: for x, y, X being ManySortedSet of st not I is empty & {x,y} \ X = {x} holds
not x in X
let x, y, X be ManySortedSet of ; :: thesis: ( not I is empty & {x,y} \ X = {x} implies not x in X )
assume that
A1: not I is empty and
A2: {x,y} \ X = {x} ; :: thesis: not x in X
consider i being set such that
A3: i in I by A1, XBOOLE_0:def 1;
{(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by A3, Def2
.= ({x,y} \ X) . i by A3, PBOOLE:def 9
.= {(x . i)} by A2, A3, Def1 ;
then not x . i in X . i by ZFMISC_1:70;
hence not x in X by A3, PBOOLE:def 4; :: thesis: verum