let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y (\) X holds
X = EmptyMS I
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y (\) X implies X = EmptyMS I )
assume A1: X c= Y (\) X ; :: thesis: X = EmptyMS I
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( i in I implies X . i = (EmptyMS I) . i )
assume A2: i in I ; :: thesis: X . i = (EmptyMS I) . i
then X . i c= (Y (\) X) . i by A1;
then X . i c= (Y . i) \ (X . i) by A2, Def6;
hence X . i = {} by XBOOLE_1:38
.= (EmptyMS I) . i by Th5 ;
:: thesis: verum