for r, t being ExtReal st r < t holds
ex s being ExtReal st
( r < s & s < t )