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