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

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