theorem Th38: :: INTERVA1:38

for U being non empty set
for A, B being non empty ordered Subset-Family of U holds DIFFERENCE (A,B) = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }