let U be non empty set ; :: thesis: Inter ({} U),({} U) is non empty IntervalSet of U
Inter ({} U),({} U) = {{} } by ThA1;
hence Inter ({} U),({} U) is non empty IntervalSet of U ; :: thesis: verum