let U be non empty set ; :: thesis: for A being Subset of U holds {A} is IntervalSet of U
let A be Subset of U; :: thesis: {A} is IntervalSet of U
Inter (A,A) = {A} by Th8;
hence {A} is IntervalSet of U by Def2; :: thesis: verum