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 A1: not {} U in Inter (([#] U),([#] U)) by Th1;
A2: {} U in Inter (({} U),([#] U)) ;
then consider A being non empty IntervalSet of U such that
A3: A = Inter (({} U),([#] U)) ;
A4: A ^ = Inter ((([#] U) `),(({} U) `)) by Th46, A3
.= Inter (({} U),([#] U)) ;
A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;
then ( (A ^) ``1 = {} U & (A ^) ``2 = [#] U ) by Th6, A4;
then (A _\/_ A) ^ = Inter ((({} U) \/ ({} U)),(([#] U) \/ ([#] U))) by Th17, A3, A4
.= Inter (({} U),([#] U)) ;
hence ex A being non empty IntervalSet of U st (A _\/_ A) ^ <> Inter (([#] U),([#] U)) by A2, A1; :: thesis: verum