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 ^ )
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 {} )
c1: A ``1 c= A ``2 by wazne2;
assume x in (A ``1 ) /\ ((A ``2 ) ` ) ; :: thesis: x in {}
then ( x in A ``1 & x in (A ``2 ) ` ) by XBOOLE_0:def 4;
hence x in {} by c1, XBOOLE_0:def 5; :: thesis: verum

end;

e1: A ^ = Inter ((A ``2 ) ` ),((A ``1 ) ` ) by ThDop0;
A ^ = Inter ((A ^ ) ``1 ),((A ^ ) ``2 ) by Wazne33;
then ( (A ^ ) ``1 = (A ``2 ) ` & (A ^ ) ``2 = (A ``1 ) ` ) by Pik, e1;
then a1: A _/\_ (A ^ ) = Inter ((A ``1 ) /\ ((A ``2 ) ` )),((A ``2 ) /\ ((A ``1 ) ` )) by Int;
( (A ``1 ) /\ ((A ``2 ) ` ) c= {} & {} c= (A ``2 ) /\ ((A ``1 ) ` ) ) by a0, XBOOLE_1:2;
hence {} in A _/\_ (A ^ ) by a1, Lemacik; :: thesis: verum