let U be non empty set ; :: thesis: ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U))
a0: [#] U in Inter (({} U),([#] U)) ;
then consider A being non empty IntervalSet of U such that
a1: A = Inter (({} U),([#] U)) ;
d2: A ^ = Inter ((([#] U) `),(({} U) `)) by a1, ThDop1
.= Inter (({} U),([#] U)) ;
A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Wazne33;
then ( (A ^) ``1 = {} U & (A ^) ``2 = [#] U ) by Pik, d2;
then a2: (A _/\_ A) ^ = Inter ((({} U) /\ ({} U)),(([#] U) /\ ([#] U))) by a1, Int, d2
.= Inter (({} U),([#] U)) ;
not [#] U c= {} U ;
then not [#] U in Inter (({} U),({} U)) by Lemacik;
hence ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U)) by a2, a0; :: thesis: verum