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