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= {}

hence {} in A _\_ A by Th1, A2, A1; :: thesis: verum

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

{} c= (A ``2) \ (A ``1)
;
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;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

hence {} in A _\_ A by Th1, A2, A1; :: thesis: verum