let U be non empty set ; :: thesis: for A, B being non empty IntervalSet of U holds A _\/_ B = Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 ))
let A, B be non empty IntervalSet of U; :: thesis: A _\/_ B = Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 ))
thus A _\/_ B c= Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) :: according to XBOOLE_0:def 10 :: thesis: Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) c= A _\/_ B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A _\/_ B or x in Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) )
assume P1: x in A _\/_ B ; :: thesis: x in Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 ))
then consider X, Y being set such that
A3: ( X in A & Y in B & x = X \/ Y ) by SETFAM_1:def 4;
A2: ( A ``1 c= X & X c= A ``2 ) by A3, Wazne;
A4: ( B ``1 c= Y & Y c= B ``2 ) by A3, Wazne;
then A5: x c= (A ``2 ) \/ (B ``2 ) by A2, A3, XBOOLE_1:13;
(A ``1 ) \/ (B ``1 ) c= x by A2, A3, A4, XBOOLE_1:13;
hence x in Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) by P1, A5; :: thesis: verum

end;

thus Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) c= A _\/_ B :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) or x in A _\/_ B )
assume x in Inter ((A ``1 ) \/ (B ``1 )),((A ``2 ) \/ (B ``2 )) ; :: thesis: x in A _\/_ B
then consider Z being Element of bool U such that
T1: ( x = Z & (A ``1 ) \/ (B ``1 ) c= Z & Z c= (A ``2 ) \/ (B ``2 ) ) ;
A ``1 c= (Z \/ (A ``1 )) /\ (A ``2 )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ``1 or x in (Z \/ (A ``1 )) /\ (A ``2 ) )
assume a0: x in A ``1 ; :: thesis: x in (Z \/ (A ``1 )) /\ (A ``2 )
assume aa: not x in (Z \/ (A ``1 )) /\ (A ``2 ) ; :: thesis: contradiction

per cases ( not x in Z \/ (A ``1 ) or not x in A ``2 ) by aa, XBOOLE_0:def 4;

suppose not x in Z \/ (A ``1 ) ; :: thesis: contradiction

hence contradiction by a0, XBOOLE_0:def 3; :: thesis: verum

end;

suppose b1: not x in A ``2 ; :: thesis: contradiction

( A ``1 c= A ``2 & x in A ``1 ) by a0, wazne2;
hence contradiction by b1; :: thesis: verum

end;

end;

end;

then ( A ``1 c= (Z \/ (A ``1 )) /\ (A ``2 ) & (Z \/ (A ``1 )) /\ (A ``2 ) c= A ``2 ) by XBOOLE_1:17;
then e1: (Z \/ (A ``1 )) /\ (A ``2 ) in A by Wazne;
B ``1 c= (Z \/ (B ``1 )) /\ (B ``2 )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B ``1 or x in (Z \/ (B ``1 )) /\ (B ``2 ) )
assume a1: x in B ``1 ; :: thesis: x in (Z \/ (B ``1 )) /\ (B ``2 )
then a2: x in Z \/ (B ``1 ) by XBOOLE_0:def 3;
B ``1 c= B ``2 by wazne2;
hence x in (Z \/ (B ``1 )) /\ (B ``2 ) by a1, a2, XBOOLE_0:def 4; :: thesis: verum

end;

then ( B ``1 c= (Z \/ (B ``1 )) /\ (B ``2 ) & (Z \/ (B ``1 )) /\ (B ``2 ) c= B ``2 ) by XBOOLE_1:17;
then e2: (Z \/ (B ``1 )) /\ (B ``2 ) in B by Wazne;
((Z \/ (A ``1 )) /\ (A ``2 )) \/ ((Z \/ (B ``1 )) /\ (B ``2 )) = (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (Z \/ (B ``1 ))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 )) by XBOOLE_1:24
.= (((Z \/ (A ``1 )) \/ (Z \/ (B ``1 ))) /\ ((A ``2 ) \/ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 )) by XBOOLE_1:24
.= ((Z \/ ((A ``1 ) \/ (B ``1 ))) /\ ((A ``2 ) \/ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 )) by XBOOLE_1:5
.= (Z /\ ((A ``2 ) \/ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 )) by T1, XBOOLE_1:12
.= ((Z /\ (A ``2 )) \/ (Z /\ (Z \/ (B ``1 )))) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 )) by XBOOLE_1:23
.= ((Z /\ (A ``2 )) \/ Z) /\ (((Z \/ (A ``1 )) /\ (A ``2 )) \/ (B ``2 )) by XBOOLE_1:28, XBOOLE_1:7
.= Z /\ ((B ``2 ) \/ ((Z \/ (A ``1 )) /\ (A ``2 ))) by XBOOLE_1:12, XBOOLE_1:17
.= Z /\ (((Z \/ (A ``1 )) \/ (B ``2 )) /\ ((A ``2 ) \/ (B ``2 ))) by XBOOLE_1:24
.= Z /\ ((Z \/ ((A ``1 ) \/ (B ``2 ))) /\ ((A ``2 ) \/ (B ``2 ))) by XBOOLE_1:4
.= Z /\ ((Z /\ ((A ``2 ) \/ (B ``2 ))) \/ (((A ``1 ) \/ (B ``2 )) /\ ((A ``2 ) \/ (B ``2 )))) by XBOOLE_1:23
.= Z /\ (Z \/ (((A ``1 ) \/ (B ``2 )) /\ ((A ``2 ) \/ (B ``2 )))) by T1, XBOOLE_1:28
.= Z /\ ((Z \/ ((A ``1 ) \/ (B ``2 ))) /\ (Z \/ ((A ``2 ) \/ (B ``2 )))) by XBOOLE_1:24
.= (Z /\ (Z \/ ((A ``1 ) \/ (B ``2 )))) /\ (Z \/ ((A ``2 ) \/ (B ``2 ))) by XBOOLE_1:16
.= Z /\ (Z \/ ((A ``2 ) \/ (B ``2 ))) by XBOOLE_1:28, XBOOLE_1:7
.= Z by XBOOLE_1:28, XBOOLE_1:7 ;
then consider X, Y being Subset of U such that
r1: ( X in A & Y in B & Z = X \/ Y ) by e1, e2;
thus x in A _\/_ B by SETFAM_1:def 4, r1, T1; :: thesis: verum

end;