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

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

thus
Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) c= A _\/_ B
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A _\/_ B or x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) )

reconsider xx = x as set by TARSKI:1;

assume A1: x in A _\/_ B ; :: thesis: x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))

then consider X, Y being set such that

A2: ( X in A & Y in B & x = X \/ Y ) by SETFAM_1:def 4;

A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;

A4: ( B ``1 c= Y & Y c= B ``2 ) by A2, Th14;

then A5: xx c= (A ``2) \/ (B ``2) by A3, A2, XBOOLE_1:13;

(A ``1) \/ (B ``1) c= xx by A3, A2, A4, XBOOLE_1:13;

hence x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) by A1, A5; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume A1: x in A _\/_ B ; :: thesis: x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))

then consider X, Y being set such that

A2: ( X in A & Y in B & x = X \/ Y ) by SETFAM_1:def 4;

A3: ( A ``1 c= X & X c= A ``2 ) by A2, Th14;

A4: ( B ``1 c= Y & Y c= B ``2 ) by A2, Th14;

then A5: xx c= (A ``2) \/ (B ``2) by A3, A2, XBOOLE_1:13;

(A ``1) \/ (B ``1) c= xx by A3, A2, A4, XBOOLE_1:13;

hence x in Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2))) by A1, A5; :: thesis: verum

proof

let x be object ; :: 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

A6: ( x = Z & (A ``1) \/ (B ``1) c= Z & Z c= (A ``2) \/ (B ``2) ) ;

A ``1 c= (Z \/ (A ``1)) /\ (A ``2)

then A10: (Z \/ (A ``1)) /\ (A ``2) in A by Th14;

B ``1 c= (Z \/ (B ``1)) /\ (B ``2)

then A13: (Z \/ (B ``1)) /\ (B ``2) in B by Th14;

((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 A6, 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:7, XBOOLE_1:28

.= 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 A6, 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:7, XBOOLE_1:28

.= Z by XBOOLE_1:7, XBOOLE_1:28 ;

then consider X, Y being Subset of U such that

A14: ( X in A & Y in B & Z = X \/ Y ) by A10, A13;

thus x in A _\/_ B by A14, A6, SETFAM_1:def 4; :: thesis: verum

end;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

A6: ( x = Z & (A ``1) \/ (B ``1) c= Z & Z c= (A ``2) \/ (B ``2) ) ;

A ``1 c= (Z \/ (A ``1)) /\ (A ``2)

proof

then
( A ``1 c= (Z \/ (A ``1)) /\ (A ``2) & (Z \/ (A ``1)) /\ (A ``2) c= A ``2 )
by XBOOLE_1:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ``1 or x in (Z \/ (A ``1)) /\ (A ``2) )

assume A7: x in A ``1 ; :: thesis: x in (Z \/ (A ``1)) /\ (A ``2)

assume A8: not x in (Z \/ (A ``1)) /\ (A ``2) ; :: thesis: contradiction

end;assume A7: x in A ``1 ; :: thesis: x in (Z \/ (A ``1)) /\ (A ``2)

assume A8: not x in (Z \/ (A ``1)) /\ (A ``2) ; :: thesis: contradiction

then A10: (Z \/ (A ``1)) /\ (A ``2) in A by Th14;

B ``1 c= (Z \/ (B ``1)) /\ (B ``2)

proof

then
( B ``1 c= (Z \/ (B ``1)) /\ (B ``2) & (Z \/ (B ``1)) /\ (B ``2) c= B ``2 )
by XBOOLE_1:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B ``1 or x in (Z \/ (B ``1)) /\ (B ``2) )

assume A11: x in B ``1 ; :: thesis: x in (Z \/ (B ``1)) /\ (B ``2)

then A12: x in Z \/ (B ``1) by XBOOLE_0:def 3;

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

hence x in (Z \/ (B ``1)) /\ (B ``2) by A11, A12, XBOOLE_0:def 4; :: thesis: verum

end;assume A11: x in B ``1 ; :: thesis: x in (Z \/ (B ``1)) /\ (B ``2)

then A12: x in Z \/ (B ``1) by XBOOLE_0:def 3;

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

hence x in (Z \/ (B ``1)) /\ (B ``2) by A11, A12, XBOOLE_0:def 4; :: thesis: verum

then A13: (Z \/ (B ``1)) /\ (B ``2) in B by Th14;

((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 A6, 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:7, XBOOLE_1:28

.= 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 A6, 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:7, XBOOLE_1:28

.= Z by XBOOLE_1:7, XBOOLE_1:28 ;

then consider X, Y being Subset of U such that

A14: ( X in A & Y in B & Z = X \/ Y ) by A10, A13;

thus x in A _\/_ B by A14, A6, SETFAM_1:def 4; :: thesis: verum