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