let U be non empty set ; :: thesis: for A being non empty IntervalSet of U holds U in A _\/_ (A ^)

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

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

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

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

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

hence U in A _\/_ (A ^) by A1; :: thesis: verum

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

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

proof

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

assume A2: x in U ; :: thesis: x in (A ``2) \/ ((A ``1) `)

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

then A3: (A ``2) ` c= (A ``1) ` by SUBSET_1:12;

( x in A ``2 or x in (A ``2) ` ) by A2, XBOOLE_0:def 5;

hence x in (A ``2) \/ ((A ``1) `) by A3, XBOOLE_0:def 3; :: thesis: verum

end;assume A2: x in U ; :: thesis: x in (A ``2) \/ ((A ``1) `)

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

then A3: (A ``2) ` c= (A ``1) ` by SUBSET_1:12;

( x in A ``2 or x in (A ``2) ` ) by A2, XBOOLE_0:def 5;

hence x in (A ``2) \/ ((A ``1) `) by A3, XBOOLE_0:def 3; :: thesis: verum

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

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

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

hence U in A _\/_ (A ^) by A1; :: thesis: verum