let A be Interval; :: 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 A1: ( A c= B \/ C & A meets B & A meets C ) ; :: thesis: B meets C
( A is open_interval or A is closed_interval or A is right_open_interval or A is left_open_interval ) by MEASURE5:1;
hence B meets C by A1, Lm1, Lm2, Lm3, Lm4; :: thesis: verum