let I, J be Interval; :: thesis: ( I is open_interval & J is closed_interval & I meets J implies I /\ J is Interval )
assume A1: ( I is open_interval & J is closed_interval & I meets J ) ; :: thesis: I /\ J is Interval
then consider p, q being R_eal such that
A2: I = ].p,q.[ ;
consider r, s being Real such that
A3: J = [.r,s.] by A1;
per cases ( ( p < r & s < q ) or ( p < r & q <= s ) or ( p >= r & q > s ) or ( p >= r & q <= s ) ) ;
suppose ( p < r & s < q ) ; :: thesis: I /\ J is Interval
hence I /\ J is Interval by A2, A3, XXREAL_1:47, 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:148;
then I /\ J is right_open_interval ;
hence I /\ J is Interval ; :: thesis: verum
end;
suppose ( p >= r & q > s ) ; :: thesis: I /\ J is Interval
then I /\ J = ].p,s.] by A2, A3, XXREAL_1:149;
then I /\ J is left_open_interval ;
hence I /\ J is Interval ; :: thesis: verum
end;
suppose ( p >= r & q <= s ) ; :: thesis: I /\ J is Interval
hence I /\ J is Interval by A2, A3, XXREAL_1:37, XBOOLE_1:28; :: thesis: verum
end;
end;