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 Th16;
thus Y \ X = (Y \/ X) \ X by Th81
.= ([[0]] I) \/ ((Y \/ X) \ X) by Th53
.= X \+\ (X \/ Y) by A1, Th58 ; :: thesis: verum