let A be closed_interval Subset of REAL; :: thesis:
let B, C be open_interval Subset of REAL; :: thesis:
assume that
A1: A c= B \/ C and
A2: A meets B and
A3: A meets C ; :: thesis:

per cases ;

suppose ( A c= B or A c= C ) ; :: thesis:

then ex x being object st
( x in A & x in B /\ C ) by A2, A3, XBOOLE_1:77, XBOOLE_0:3;
hence B meets C by XBOOLE_0:4; :: thesis:

end;

suppose A4: ( not A c= B & not A c= C ) ; :: thesis:

A5: ( A <> {} & B <> {} & C <> {} ) by A2, A3, XBOOLE_1:65;
then consider a1, a2 being Real such that
A6: ( a1 <= a2 & A = [.a1,a2.] ) by MEASURE5:14;
consider b1, b2 being R_eal such that
A7: B = ].b1,b2.[ by MEASURE5:def 2;
consider c1, c2 being R_eal such that
A8: C = ].c1,c2.[ by MEASURE5:def 2;
A9: ( b1 < a2 & a1 < b2 ) by A2, A6, A7, XXREAL_1:89, XXREAL_1:93;

per cases by A4, A6, A7, XXREAL_1:47;

suppose a1 <= b1 ; :: thesis:

then A10: b1 in B \/ C by A1, A6, A9, XXREAL_1:1;
not b1 in B by A7, XXREAL_1:4;
then b1 in C by A10, XBOOLE_0:def 3;
then A11: ( c1 < b1 & b1 < c2 ) by A8, XXREAL_1:4;
then consider x being Real such that
A12: ( b1 < x & x < c2 ) by XXREAL_3:3;

per cases ;

suppose b2 < c2 ; :: thesis:

hence B meets C by A5, A7, A8, A11, XXREAL_1:46, XBOOLE_1:69; :: thesis:

end;

suppose c2 <= b2 ; :: thesis:

then ( x < b2 & c1 < x ) by A11, A12, XXREAL_0:2;
then ( x in B & x in C ) by A7, A8, A12, XXREAL_1:4;
hence B meets C by XBOOLE_0:3; :: thesis:

end;

end;

end;

suppose b2 <= a2 ; :: thesis:

then A13: b2 in B \/ C by A1, A6, A9, XXREAL_1:1;
not b2 in B by A7, XXREAL_1:4;
then b2 in C by A13, XBOOLE_0:def 3;
then A14: ( c1 < b2 & b2 < c2 ) by A8, XXREAL_1:4;
then consider x being Real such that
A15: ( c1 < x & x < b2 ) by XXREAL_3:3;

per cases ;

suppose c1 < b1 ; :: thesis:

hence B meets C by A5, A7, A8, A14, XXREAL_1:46, XBOOLE_1:69; :: thesis:

end;

suppose b1 <= c1 ; :: thesis:

then ( b1 < x & x < c2 ) by A14, A15, XXREAL_0:2;
then ( x in B & x in C ) by A7, A8, A15, XXREAL_1:4;
hence B meets C by XBOOLE_0:3; :: thesis:

end;

end;

end;

end;

end;

end;