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 ThA1;
hence {A} is IntervalSet of U by WW; :: thesis: verum