let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y holds
Y = X \/ (Y \ X)
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y implies Y = X \/ (Y \ X) )
assume A1: X c= Y ; :: thesis: Y = X \/ (Y \ X)
thus Y = (Y \ X) \/ (Y /\ X) by Th65
.= X \/ (Y \ X) by A1, Th23 ; :: thesis: verum