theorem :: XXREAL_1:272

for a, b being Real holds ].-infty,a.] /\ [.b,+infty.[ = [.b,a.]