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 Th1;
then consider A being non empty IntervalSet of U such that
A1: A = Inter (({} U),([#] U)) ;
A2: A _\_ A = Inter ((({} U) \ ([#] U)),(([#] U) \ ({} U))) by Th42, A1
.= Inter (({} U),([#] U)) ;
not U c= {} ;
then ( [#] U in Inter (({} U),([#] U)) & not [#] U in Inter (({} U),({} U)) ) by Th1;
hence ex A being non empty IntervalSet of U st A _\_ A <> Inter (({} U),({} U)) by A2; :: thesis: verum