let I, J be Interval; ( 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 )
; 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
; verum