let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y holds
( X \/ Y = Y & Y \/ X = Y )
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y implies ( X \/ Y = Y & Y \/ X = Y ) )
assume A1: X c= Y ; :: thesis: ( X \/ Y = Y & Y \/ X = Y )
hence X \/ Y c= Y by Th18; :: according to PBOOLE:def 10 :: thesis: ( Y c= X \/ Y & Y \/ X = Y )
thus Y c= X \/ Y by Th16; :: thesis: Y \/ X = Y
thus Y \/ X c= Y by A1, Th18; :: according to PBOOLE:def 10 :: thesis: Y c= Y \/ X
thus Y c= Y \/ X by Th16; :: thesis: verum