theorem Th6: :: EXCHSORT:6

for a, b being Ordinal st a \ b <> {} holds
( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )