let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds {} in A _\_ A
let A be non empty IntervalSet of U; :: thesis: {} in A _\_ A
A1: A _\_ A = Inter (((A ``1) \ (A ``2)),((A ``2) \ (A ``1))) by Th40;
A2: (A ``1) \ (A ``2) c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ``1) \ (A ``2) or x in {} )
assume x in (A ``1) \ (A ``2) ; :: thesis: x in {}
then ( x in A ``1 & not x in A ``2 & A ``1 c= A ``2 ) by Th16, XBOOLE_0:def 5;
hence x in {} ; :: thesis: verum

end;

{} c= (A ``2) \ (A ``1) ;
hence {} in A _\_ A by Th1, A2, A1; :: thesis: verum