let I, J be Interval; :: thesis: ( I is right_open_interval & J is left_open_interval & I meets J implies I /\ J is Interval )
assume A1: ( I is right_open_interval & J is left_open_interval & I meets J ) ; :: thesis: I /\ J is Interval
then consider p being Real, q being R_eal such that
A2: I = [.p,q.[ ;
consider r being R_eal, s being Real such that
A3: J = ].r,s.] by A1;

per cases ( ( r < p & s < q ) or ( r < p & q <= s ) or ( p <= r & q <= s ) or ( p <= r & s < q ) ) ;

suppose ( r < p & s < q ) ; :: thesis: I /\ J is Interval

then I /\ J = [.p,s.] by A2, A3, XXREAL_1:152;
then I /\ J is closed_interval ;
hence I /\ J is Interval ; :: thesis: verum

end;

suppose ( r < p & q <= s ) ; :: thesis: I /\ J is Interval

hence I /\ J is Interval by A2, A3, XXREAL_1:40, XBOOLE_1:28; :: thesis: verum

end;

suppose ( p <= r & q <= s ) ; :: thesis: I /\ J is Interval

then I /\ J = ].r,q.[ by A2, A3, XXREAL_1:153;
then I /\ J is open_interval ;
hence I /\ J is Interval ; :: thesis: verum

end;

suppose ( p <= r & s < q ) ; :: thesis: I /\ J is Interval

hence I /\ J is Interval by A2, A3, XXREAL_1:44, XBOOLE_1:28; :: thesis: verum

end;

end;