for X being set
for A1 being SetSequence of X st A1 is non-descending holds
Partial_Union A1 = A1 by Lm2;