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