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