consider A being Subset of U;
{A} is IntervalSet of U by ThB1;
hence not for b₁ being IntervalSet of U holds b₁ is empty ; :: thesis: verum