let I, J be Interval; :: thesis: ( I is closed_interval & J is right_open_interval & I meets J implies I /\ J is Interval )
assume A1: ( I is closed_interval & J is right_open_interval & I meets J ) ; :: thesis: I /\ J is Interval
then consider p, q being Real such that
A2: I = [.p,q.] ;
consider r being Real, s being R_eal such that
A3: J = [.r,s.[ by A1;
per cases ( ( r <= p & s <= q ) or ( r <= p & s > q ) or ( r > p & s <= q ) or ( r > p & s > q ) ) ;
suppose ( r <= p & s <= q ) ; :: thesis: I /\ J is Interval
then I /\ J = [.p,s.[ by A2, A3, XXREAL_1:144;
then I /\ J is right_open_interval ;
hence I /\ J is Interval ; :: thesis: verum
end;
suppose ( r <= p & s > q ) ; :: thesis: I /\ J is Interval
hence I /\ J is Interval by A2, A3, XXREAL_1:43, XBOOLE_1:28; :: thesis: verum
end;
suppose ( r > p & s <= q ) ; :: thesis: I /\ J is Interval
hence I /\ J is Interval by A2, A3, XXREAL_1:35, XBOOLE_1:28; :: thesis: verum
end;
suppose ( r > p & s > q ) ; :: thesis: I /\ J is Interval
then I /\ J = [.r,q.] by A2, A3, XXREAL_1:145;
then I /\ J is closed_interval ;
hence I /\ J is Interval ; :: thesis: verum
end;
end;