let I, J be Subset of REAL; :: thesis: ( I is right_open_interval & J is right_open_interval implies I /\ J is right_open_interval )
assume A1: ( I is right_open_interval & J is right_open_interval ) ; :: thesis: I /\ J is right_open_interval
then consider p being Real, q being R_eal such that
A2: I = [.p,q.[ ;
consider r being Real, s being R_eal such that
A3: J = [.r,s.[ by A1;
A4: min (s,q) is R_eal by XXREAL_0:def 1;
I /\ J = [.(max (r,p)),(min (s,q)).[ by A2, A3, XXREAL_1:139;
hence I /\ J is right_open_interval by A4; :: thesis: verum