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

A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;

then ( (A ^) ``1 = (A ``2) ` & (A ^) ``2 = (A ``1) ` ) by Th6, A3;

then A4: A _/\_ (A ^) = Inter (((A ``1) /\ ((A ``2) `)),((A ``2) /\ ((A ``1) `))) by Th18;

( (A ``1) /\ ((A ``2) `) c= {} & {} c= (A ``2) /\ ((A ``1) `) ) by A1;

hence {} in A _/\_ (A ^) by A4, Th1; :: thesis: verum

let A be non empty IntervalSet of U; :: thesis: {} in A _/\_ (A ^)

A1: (A ``1) /\ ((A ``2) `) c= {}

proof

A3:
A ^ = Inter (((A ``2) `),((A ``1) `))
by Th45;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ``1) /\ ((A ``2) `) or x in {} )

A2: A ``1 c= A ``2 by Th16;

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 A2, XBOOLE_0:def 5; :: thesis: verum

end;A2: A ``1 c= A ``2 by Th16;

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 A2, XBOOLE_0:def 5; :: thesis: verum

A ^ = Inter (((A ^) ``1),((A ^) ``2)) by Th15;

then ( (A ^) ``1 = (A ``2) ` & (A ^) ``2 = (A ``1) ` ) by Th6, A3;

then A4: A _/\_ (A ^) = Inter (((A ``1) /\ ((A ``2) `)),((A ``2) /\ ((A ``1) `))) by Th18;

( (A ``1) /\ ((A ``2) `) c= {} & {} c= (A ``2) /\ ((A ``1) `) ) by A1;

hence {} in A _/\_ (A ^) by A4, Th1; :: thesis: verum