let A be left_open_interval Subset of REAL; :: thesis: for B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds
B meets C
let B, C be open_interval Subset of REAL; :: thesis: ( A c= B \/ C & A meets B & A meets C implies B meets C )
assume that
A1: A c= B \/ C and
A2: A meets B and
A3: A meets C ; :: thesis: B meets C

per cases ( A c= B or A c= C or ( not A c= B & not A c= C ) ) ;

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

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: verum

end;

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

A5: ( A <> {} & B <> {} & C <> {} ) by A2, A3, XBOOLE_1:65;
consider a1 being R_eal, a2 being Real such that
A6: A = ].a1,a2.] by MEASURE5:def 5;
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:91, XXREAL_1:276;

per cases ( a1 < b1 or b2 <= a2 ) by A4, A6, A7, XXREAL_1:49;

suppose a1 < b1 ; :: thesis: B meets C

then A10: b1 in B \/ C by A1, A6, A9, XXREAL_1:2;
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 ( b2 < c2 or c2 <= b2 ) ;

suppose b2 < c2 ; :: thesis: B meets C

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

end;

suppose c2 <= b2 ; :: thesis: B meets C

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: verum

end;

end;

end;

suppose b2 <= a2 ; :: thesis: B meets C

then A13: b2 in B \/ C by A1, A6, A9, XXREAL_1:2;
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 ( c1 < b1 or b1 <= c1 ) ;

suppose c1 < b1 ; :: thesis: B meets C

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

end;

suppose b1 <= c1 ; :: thesis: B meets C

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: verum

end;

end;

end;

end;

end;

end;