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