let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
let X, Y, Z be ManySortedSet of I; :: thesis: X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
A1: X \ Y c= X by Th62;
thus X \ (Y \/ Z) = (X \ Y) \ Z by Th79
.= ((X \ Y) /\ X) \ Z by A1, Th25
.= (X \ Y) /\ (X \ Z) by Th68 ; :: thesis: verum