let I be set ; :: thesis: for X, Y being ManySortedSet of I holds
( X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X )
let X, Y be ManySortedSet of I; :: thesis: ( X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X )
X c= X \/ Y by Th16;
then A1: X c= X /\ (X \/ Y) by Th19;
A2: X /\ (X \/ Y) c= X by Th17;
hence X /\ (X \/ Y) = X by A1, Def13; :: thesis: ( (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X )
thus (X \/ Y) /\ X = X by A2, A1, Def13; :: thesis: ( X /\ (Y \/ X) = X & (Y \/ X) /\ X = X )
thus ( X /\ (Y \/ X) = X & (Y \/ X) /\ X = X ) by A2, A1, Def13; :: thesis: verum