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