let I be set ; :: thesis: for Y, X being ManySortedSet of I holds Y \ X = X \+\ (X \/ Y)
let Y, X be ManySortedSet of I; :: thesis: Y \ X = X \+\ (X \/ Y)
A1: X c= Y \/ X by Th14;
thus Y \ X = (Y \/ X) \ X by Th75
.= ([[0]] I) \/ ((Y \/ X) \ X) by Th22, Th43
.= X \+\ (X \/ Y) by A1, Th52 ; :: thesis: verum