let U be non empty set ; :: thesis: Inter (({} U),({} U)) is non empty IntervalSet of U
Inter (({} U),({} U)) = {{}} by Th8;
hence Inter (({} U),({} U)) is non empty IntervalSet of U ; :: thesis: verum