let I be set ; :: thesis: for X, Y being ManySortedSet of holds
( X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X )
let X, Y be ManySortedSet of ; :: thesis: ( X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X )
thus A1: X \/ (X /\ Y) = X :: thesis: ( (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X )

proof

( X c= X & X /\ Y c= X ) by Th17;
hence X \/ (X /\ Y) c= X by Th18; :: according to PBOOLE:def 13 :: thesis: X c= X \/ (X /\ Y)
thus X c= X \/ (X /\ Y) by Th16; :: thesis: verum

end;

hence (X /\ Y) \/ X = X ; :: thesis: ( X \/ (Y /\ X) = X & (Y /\ X) \/ X = X )
thus ( X \/ (Y /\ X) = X & (Y /\ X) \/ X = X ) by A1; :: thesis: verum