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

thus X /\ (X \/ Y) c= X by Th17; :: according to PBOOLE:def 13 :: thesis: X c= X /\ (X \/ Y)
( X c= X & X c= X \/ Y ) by Th16;
hence X c= X /\ (X \/ Y) by Th19; :: 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