let U be non empty set ; :: thesis: ex A being non empty IntervalSet of U st A _\_ A <> Inter ({} U),({} U)
Inter ({} U),([#] U) <> {} by Lemacik;
then consider A being non empty IntervalSet of U such that
a1: A = Inter ({} U),([#] U) ;
a3: A _\_ A = Inter (({} U) \ ([#] U)),(([#] U) \ ({} U)) by Dif3, a1
.= Inter ({} U),([#] U) ;
not U c= {} ;
then ( [#] U in Inter ({} U),([#] U) & not [#] U in Inter ({} U),({} U) ) by Lemacik;
hence ex A being non empty IntervalSet of U st A _\_ A <> Inter ({} U),({} U) by a3; :: thesis: verum