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 ^ )
b1: U c= (A ``2 ) \/ ((A ``1 ) ` )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in (A ``2 ) \/ ((A ``1 ) ` ) )
assume c1: x in U ; :: thesis: x in (A ``2 ) \/ ((A ``1 ) ` )
A ``1 c= A ``2 by wazne2;
then c2: (A ``2 ) ` c= (A ``1 ) ` by SUBSET_1:31;
( x in A ``2 or x in (A ``2 ) ` ) by c1, XBOOLE_0:def 5;
hence x in (A ``2 ) \/ ((A ``1 ) ` ) by c2, XBOOLE_0:def 3; :: thesis: verum

end;

a1: A ^ = Inter ((A ``2 ) ` ),((A ``1 ) ` ) by ThDop0;
A ^ = Inter ((A ^ ) ``1 ),((A ^ ) ``2 ) by Wazne33;
then ab: ( (A ^ ) ``1 = (A ``2 ) ` & (A ^ ) ``2 = (A ``1 ) ` ) by Pik, a1;
A _\/_ (A ^ ) = Inter ((A ``1 ) \/ ((A ``2 ) ` )),((A ``2 ) \/ ((A ``1 ) ` )) by ab, Un;
hence U in A _\/_ (A ^ ) by b1; :: thesis: verum