let I be set ; :: thesis: for X, Y being ManySortedSet of I st X \ Y = Y \ X holds
X = Y
let X, Y be ManySortedSet of I; :: thesis: ( X \ Y = Y \ X implies X = Y )
assume X \ Y = Y \ X ; :: thesis: X = Y
hence X = (Y \ X) \/ (Y /\ X) by Th71
.= Y by Th71 ;
:: thesis: verum