let U be non empty set ; 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; verum