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