theorem Th3: :: INTEGR19:3

for X being set
for a, b, c, d being Real st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X holds
['(min (c,d)),(max (c,d))'] c= X