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