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