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
b0: A _\_ A = Inter ((A ``1 ) \ (A ``2 )),((A ``2 ) \ (A ``1 )) by Dif;
a0: (A ``1 ) \ (A ``2 ) c= {}

proof

let x be set ; :: 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 wazne2, XBOOLE_0:def 5;
hence x in {} ; :: thesis: verum

end;

{} c= (A ``2 ) \ (A ``1 ) by XBOOLE_1:2;
hence {} in A _\_ A by Lemacik, a0, b0; :: thesis: verum