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