let I, J be Interval; :: thesis: ( I is open_interval & J is open_interval & I meets J implies I /\ J is Interval )
assume A1: ( I is open_interval & J is open_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 R_eal such that
A3: J = ].r,s.[ by A1;
A4: I /\ J = ].(max (p,r)),(min (q,s)).[ by A2, A3, XXREAL_1:142;
( max (p,r) is R_eal & min (q,s) is R_eal ) by XXREAL_0:def 1;
then I /\ J is open_interval by A4;
hence I /\ J is Interval ; :: thesis: verum