theorem :: XREAL_1:4

for a, b being Real ex c being Real st
( c < a & c < b )