let I, J be Interval; :: thesis: ( I is left_open_interval & J is left_open_interval & I meets J implies I /\ J is Interval )
assume A1: ( I is left_open_interval & J is left_open_interval & I meets J ) ; :: thesis: I /\ J is Interval
then consider p being R_eal, q being Real such that
A2: I = ].p,q.] ;
consider r being R_eal, s being Real such that
A3: J = ].r,s.] by A1;
A4: I /\ J = ].(max (p,r)),(min (q,s)).] by A2, A3, XXREAL_1:141;
( max (p,r) is R_eal & min (q,s) is Real ) by XXREAL_0:def 1;
then I /\ J is left_open_interval by A4;
hence I /\ J is Interval ; :: thesis: verum