theorem :: PBOOLE:26

for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y (\/) Z iff ( Y c= X & Z c= X & ( for V being ManySortedSet of I st Y c= V & Z c= V holds
X c= V ) ) )