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